Theorem isLeftRegular_natCast

Modification history

2026-09-01 11:46
Mathlib/Algebra/Module/Torsion/Free.lean
feat(Algebra/Regular/SMul): regularity of `Nat.cast` elements (#43277) …
Added isLeftRegular_natCastView on Github →