Theorems · Theorem · commutative algebra
Ideal.span_singleton_generator
∀ {R : Type u} [inst : Semiring R] (I : Ideal R) [inst_1 : Submodule.IsPrincipal I],
Ideal.span {Submodule.IsPrincipal.generator I} = I- Defined in
- Mathlib.RingTheory.PrincipalIdealDomain
- Cited by
- 17 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- Idealstatement and proof · cited by 4,748
- Ideal.spanstatement · cited by 948
- Submodule.IsPrincipalstatement and proof · cited by 129
- Submodule.IsPrincipal.generatorstatement · cited by 56
- Submodule.IsPrincipal.principalproof · cited by 10
Cited by17
Results whose statement or proof uses this declaration.
- IsBezout.span_gcdproof · cited by 5
- Polynomial.span_singleton_annIdealGeneratorproof · cited by 4
- Ideal.relNorm_algebraMapproof · cited by 4
- Ideal.torsionOf_eq_span_pow_pOrderproof · cited by 2
- Submodule.IsPrincipal.map_ringHomproof · cited by 2
- Submodule.isInternal_prime_power_torsion_of_pidproof · cited by 1
- Rat.HeightOneSpectrum.span_natGeneratorproof · cited by 1
- Submodule.IsPrincipal.contentIdeal_le_span_iff_dvdproof · cited by 1
- Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRingproof · cited by 1
- IsDiscreteValuationRing.ideal_eq_span_pow_irreducibleproof · cited by 1
- Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_topproof · cited by 1
- Ideal.spanNorm_spanNormproof · cited by 1