Theorem Ideal.Quotient.mk_span_range

Modification history

2025-11-14 17:31
Mathlib/RingTheory/Ideal/Quotient/Basic.lean
feat(Algebra/Homology): sandwich a comm group between two finite comm groups (#31227) …
Modified Ideal.Quotient.mk_span_rangeView on Github →
2025-10-07 08:33
Mathlib/RingTheory/Ideal/Quotient/Basic.lean
feat(RingTheory/Presentation): core of a presentation (#24794) …
Added Ideal.Quotient.mk_span_rangeView on Github →