Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-09 02:37 34b61e3d

View on Github →

chore(algebra/regular/*): generalisation linter (#13955)

Estimated changes

Modified src/algebra/regular/basic.lean

Modified src/algebra/regular/smul.lean

modified theorem is_smul_regular.mul

modified theorem is_smul_regular.mul_and_mul_iff

modified theorem is_smul_regular.mul_iff_right

modified theorem is_smul_regular.of_mul