Theorem IsSMulRegular.isSMulRegular_of_injective_of_isSMulRegular

Modification history

2024-06-05 04:24
Mathlib/Algebra/Regular/SMul.lean
Ring-specific lemmas about regular elements (#13360) …
Deleted IsSMulRegular.isSMulRegular_of_injective_of_isSMulRegularView on Github →
2024-05-23 18:50
Mathlib/Algebra/Regular/SMul.lean
Feat(Algebra/Regular/SMul): Add some lemmas about `IsSMulRegular` (#13123) …
Added IsSMulRegular.isSMulRegular_of_injective_of_isSMulRegularView on Github →