Theorems · Theorem · commutative algebra
Nat.maximalIdeal_eq_span_two_three
IsLocalRing.maximalIdeal ℕ = Ideal.span {2, 3}- Defined in
- Mathlib.RingTheory.Ideal.NatInt
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 71 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Idealstatement · cited by 4,748
- le_antisymmproof · cited by 2,068
- Ideal.spanstatement and proof · cited by 948
- IsLocalRing.maximalIdealstatement and proof · cited by 297
- ZeroMemClass.zero_memproof · cited by 162
- Ne.lt_or_gtproof · cited by 108
- Ideal.span_leproof · cited by 70
- Set.pair_subsetproof · cited by 4
- Ideal.mem_span_pairproof · cited by 4
- Nat.exists_add_mul_eq_of_gcd_dvd_of_mul_pred_leproof · cited by 3
- Nat.mem_maximalIdeal_iffproof · cited by 2
Cited by1
Results whose statement or proof uses this declaration.
- ringKrullDim_natproof · cited by 0