Theorem IsLeftRegular.mul_left_eq_self_iff

Modification history

2025-09-01 13:46
Mathlib/Algebra/Regular/Basic.lean
feat(DedekindDomain): Monoid of ideals is torsion-free (#28169) …
Added IsLeftRegular.mul_left_eq_self_iffView on Github →