Commit 2026-09-01 11:46 3a72ac36

View on Github →

feat(Algebra/Regular/SMul): regularity of Nat.cast elements (#43277) IsRegular/IsLeftRegular/IsRightRegular for (n : R) are all equivalent to IsSMulRegular R n.

Estimated changes

Modified Mathlib/Algebra/Module/Torsion/Free.lean

added theorem isLeftRegular_natCast

added theorem isRegular_natCast

added theorem isRightRegular_natCast

Modified Mathlib/Algebra/Regular/SMul.lean

added theorem IsSMulRegular.nat_of_isAddTorsionFree

added theorem isAddTorsionFree_iff'