Theorems · Theorem · commutative algebra
Ideal.span_singleton_le_span_singleton
∀ {α : Type u} [inst : CommSemiring α] {x y : α}, Ideal.span {x} ≤ Ideal.span {y} ↔ y ∣ x- Defined in
- Mathlib.RingTheory.Ideal.Span
- Cited by
- 15 results in Mathlib
- Foundations
- Depth 29 from the axioms · uses propext, Quot.sound
- Assumes
- CommSemiring
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
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement · cited by 4,748
- Ideal.spanstatement · cited by 948
- Set.singleton_subset_iffproof · cited by 206
- Ideal.span_leproof · cited by 70
- Ideal.mem_span_singletonproof · cited by 69
Cited by15
Results whose statement or proof uses this declaration.
- Ideal.span_singleton_eq_span_singletonproof · cited by 15
- Ideal.span_singleton_eq_topproof · cited by 10
- PrincipalIdealRing.isMaximal_of_irreducibleproof · cited by 4
- Ideal.span_singleton_lt_span_singletonproof · cited by 4
- IsBezout.dvd_gcdproof · cited by 2
- IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_oneproof · cited by 1
- Submodule.IsPrincipal.contentIdeal_le_span_iff_dvdproof · cited by 1
- Ring.ord_le_ord_mulproof · cited by 1
- generator_maximal_submoduleImage_dvdproof · cited by 1
- Ideal.singleton_span_mem_normalizedFactors_of_mem_normalizedFactorsproof · cited by 1
- Ideal.factors_decreasingproof · cited by 0
- Submodule.IsPrincipal.contentIdeal_eq_span_content_of_isPrincipalproof · cited by 0