Theorem Ideal.exists_disjoint_powers_of_span_eq_top

Modification history

2024-11-25 11:04
Mathlib/RingTheory/Ideal/Maximal.lean
feat(RingTheory/LocalProperties): Add theorems about LocalizedModule (#19080) …
Added Ideal.exists_disjoint_powers_of_span_eq_topView on Github →