Theorems · Theorem · commutative algebra
Ideal.span_singleton_mul_span_singleton
∀ {R : Type u} [inst : Semiring R] (r s : R) [(Ideal.span {r}).IsTwoSided],
Ideal.span {r} * Ideal.span {s} = Ideal.span {r * s}- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 12 results in Mathlib
- Foundations
- Depth 73 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- SemiringIdeal.IsTwoSided
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 and proof · cited by 53,352
- Semiringstatement and proof · cited by 13,802
- Idealstatement and proof · cited by 4,748
- Ideal.spanstatement and proof · cited by 948
- Ideal.IsTwoSidedstatement and proof · cited by 179
- Set.singleton_mul_singletonproof · cited by 7
- Ideal.span_mul_span'proof · cited by 4
Cited by12
Results whose statement or proof uses this declaration.
- Ideal.span_singleton_powproof · cited by 19
- Ideal.isIdempotentElem_iff_of_fgproof · cited by 5
- FractionalIdeal.count_mulproof · cited by 4
- ClassGroup.mk_eq_one_of_coe_idealproof · cited by 2
- Ideal.associatesEquivIsPrincipal_mulproof · cited by 1
- Ideal.isOka_isPrincipalproof · cited by 1
- IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipalproof · cited by 1
- WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdealproof · cited by 1
- Ideal.isPrimary_of_isMaximal_radicalproof · cited by 0
- Ideal.squarefree_span_singletonproof · cited by 0
- Ideal.spanNorm_mulproof · cited by 0
- IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'proof · cited by 0