Theorem Ideal.subtype_isoBaseOfIsPrincipal_eq_mul

Modification history

2025-09-15 21:27
Mathlib/RingTheory/Ideal/IsPrincipal.lean
feat(RingTheory/Flat): Add theorems relating Submodule.torsion and Module.Flat (#26783)
Added Ideal.subtype_isoBaseOfIsPrincipal_eq_mulView on Github →