Commit 2022-12-22 01:22 84b62005

View on Github →

Feat: port algebra.regular.smul (#1154) Port of algebra.regular.smul Based on 550b58538991c8977703fdeb7c9d51a5aa27df11

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Regular/SMul.lean

added theorem IsLeftRegular.isSMulRegular

added theorem IsRightRegular.isSMulRegular

added theorem IsSMulRegular.isLeftRegular

added theorem IsSMulRegular.isRightRegular

added theorem IsSMulRegular.mul

added theorem IsSMulRegular.mul_and_mul_iff

added theorem IsSMulRegular.mul_iff

added theorem IsSMulRegular.mul_iff_right

added theorem IsSMulRegular.not_zero

added theorem IsSMulRegular.not_zero_iff

added theorem IsSMulRegular.of_mul

added theorem IsSMulRegular.of_mul_eq_one

added theorem IsSMulRegular.of_smul

added theorem IsSMulRegular.of_smul_eq_one

added theorem IsSMulRegular.one

added theorem IsSMulRegular.pow

added theorem IsSMulRegular.pow_iff

added theorem IsSMulRegular.smul

added theorem IsSMulRegular.smul_iff

added theorem IsSMulRegular.zero

added theorem IsSMulRegular.zero_iff_subsingleton

added def IsSMulRegular

added theorem IsUnit.isSMulRegular

added theorem Units.isSMulRegular

added theorem isLeftRegular_iff

added theorem isRightRegular_iff

added theorem isSMulRegular_of_group