Theorem IsSMulRegular.eq_zero_of_smul_eq_zero

Modification history

2025-08-11 11:23
Mathlib/Algebra/Regular/SMul.lean
feat(Algebra): connect IsRegular/IsCancelMul to nonZeroDivisors/NoZeroDivisors (#27877) …
Deleted IsSMulRegular.eq_zero_of_smul_eq_zeroView on Github →
2024-05-23 18:50
Mathlib/Algebra/Regular/SMul.lean
Feat(Algebra/Regular/SMul): Add some lemmas about `IsSMulRegular` (#13123) …
Added IsSMulRegular.eq_zero_of_smul_eq_zeroView on Github →