Mathlib v3 is deprecated. Go to Mathlib v4

Def nsmul

Modification history

2021-04-14 08:29

src/algebra/group_power/basic.lean

refactor(*): kill nat multiplication diamonds (#7084) …

Deleted nsmul View on Github →

2020-09-10 14:56

src/algebra/group_power/basic.lean

chore(*): update to Lean 3.20.0c, account for nat.pow removal from core (#3985) …

Modified nsmul View on Github →

2020-05-31 04:59

src/algebra/group_power.lean

chore(algebra/group_hom): rename `add_monoid.smul` to `nsmul` (#2861) …

Added nsmul View on Github →