Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_submonoid.mem_multiples_iff

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.mem_multiples_iffView on Github →
2021-08-11 14:09
src/group_theory/submonoid/membership.lean
chore(group_theory/submonoid/membership): missing rfl lemmas (#8619)
Added add_submonoid.mem_multiples_iffView on Github →