Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-01 20:56 9fcf391e

View on Github →

chore(group_theory/group_action/basic): relax monoid to mul_one_class (#15051)

Estimated changes

Modified src/group_theory/group_action/defs.lean

modified theorem smul_one_mul