Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.powers_one

Modification history

2022-11-25 11:49
src/group_theory/submonoid/membership.lean
feat(group_theory/submonoid): add `submonoid.powers_one` (#17692) …
Added submonoid.powers_oneView on Github →