Theorem IsSMulRegular.of_injective

Modification history

2025-08-11 11:23

Mathlib/Algebra/Regular/SMul.lean

feat(Algebra): connect IsRegular/IsCancelMul to nonZeroDivisors/NoZeroDivisors (#27877) …

Modified IsSMulRegular.of_injective View on Github →

2024-06-05 04:24

Mathlib/Algebra/Regular/SMul.lean

Ring-specific lemmas about regular elements (#13360) …

Added IsSMulRegular.of_injective View on Github →