Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-01 08:58 873f2685

View on Github →

chore(group_theory/group_action/*): generalisation linter (#13100)

Estimated changes

Modified src/group_theory/group_action/basic.lean

Modified src/group_theory/group_action/defs.lean

modified theorem mul_smul_one

Modified src/group_theory/group_action/opposite.lean

Modified src/group_theory/group_action/prod.lean

Modified src/group_theory/group_action/sub_mul_action.lean