Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_submonoid.multiples_eq_closure

Modification history

2022-11-25 11:49
src/group_theory/submonoid/membership.lean
feat(group_theory/submonoid): add `submonoid.powers_one` (#17692) …
Deleted add_submonoid.multiples_eq_closureView on Github →
2020-08-02 16:01
src/group_theory/submonoid/membership.lean
chore(group_theory/*): refactor quotient groups to use bundled subgroups (#3321)
Added add_submonoid.multiples_eq_closureView on Github →