Theorems · Definition · commutative algebra
Ideal
(R : Type u) → [Semiring R] → Type u
A (left) ideal in a semiring R is an additive submonoid s such that
a * b ∈ s whenever b ∈ s. If R is a ring, then s is an additive subgroup.
- Defined in
- Mathlib.RingTheory.Ideal.Defs
- Cited by
- 4,748 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 126 definitions · uses no axioms
- Assumes
- Semiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by5,551
Results whose statement or proof uses this declaration.
- Ideal.spanstatement · cited by 948
- Ideal.IsPrimestatement · cited by 827
- Ideal.mapstatement and proof · cited by 692
- Ideal.Quotient.mkstatement and proof · cited by 610
- Ideal.primeComplstatement and proof · cited by 462
- Ideal.IsMaximalstatement · cited by 452
- Ideal.comapstatement and proof · cited by 443
- RingHom.kerstatement · cited by 363
- PrimeSpectrum.asIdealstatement · cited by 333
- Localization.AtPrimestatement and proof · cited by 299
- IsLocalRing.maximalIdealstatement · cited by 297
- Ideal.LiesOverstatement · cited by 272
Showing the 200 most cited of 5,551.