Theorem Ideal.span_pair_eq_span_left_iff_dvd

Modification history

2025-10-06 17:04
Mathlib/RingTheory/Ideal/Span.lean
feat(RingTheory/Noetherian): add `IsNoetherianRing.of_prime` (#28451) …
Modified Ideal.span_pair_eq_span_left_iff_dvdView on Github →
2025-07-10 03:45
Mathlib/RingTheory/Ideal/Span.lean
feat(NumberField): specialized version of Kummer Dedekind for the splitting of prime numbers (part 1) (#26137) …
Added Ideal.span_pair_eq_span_left_iff_dvdView on Github →