Theorems · Theorem · commutative algebra
Ideal.span_singleton_dvd_span_singleton_iff_dvd
∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R},
Ideal.span {a} ∣ Ideal.span {b} ↔ a ∣ b- Cited by
- 6 results in Mathlib
- Foundations
- Depth 145 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Idealstatement · cited by 4,748
- IsDomainstatement and proof · cited by 2,196
- Ideal.spanstatement and proof · cited by 948
- IsPrincipalIdealRingstatement and proof · cited by 131
- dvd_reflproof · cited by 97
- Ideal.mem_span_singletonproof · cited by 69
- dvd_transproof · cited by 50
- Ideal.dvd_iff_leproof · cited by 33
Cited by6
Results whose statement or proof uses this declaration.
- RingOfIntegers.not_dvd_exponent_iffproof · cited by 4
- Ideal.emultiplicity_eq_emultiplicity_spanproof · cited by 3
- LaurentSeries.intValuation_le_iff_coeff_lt_eq_zeroproof · cited by 3
- Ideal.squarefree_span_singletonproof · cited by 0
- LaurentSeries.coeff_zero_of_lt_intValuationproof · cited by 0
- span_singleton_dvd_span_singleton_iff_dvdproof · cited by 0