Commit 2024-05-23 18:50 31ac4896

View on Github →

Feat(Algebra/Regular/SMul): Add some lemmas about IsSMulRegular (#13123) Add some lemmas about IsSMulRegular.

Estimated changes

Modified Mathlib/Algebra/Regular/SMul.lean

added theorem Equiv.isSMulRegular_congr

added theorem IsSMulRegular.eq_zero_of_smul_eq_zero

added theorem IsSMulRegular.isSMulRegular_of_injective_of_isSMulRegular