Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_cyclic.exists_monoid_generator

Modification history

2022-08-17 14:53
src/group_theory/specific_groups/cyclic.lean
chore(group_theory/*): Fix lint (#16095) …
Modified is_cyclic.exists_monoid_generatorView on Github →
2021-04-07 02:18
src/group_theory/order_of_element.lean
chore(group_theory/specific_groups/*): new folder specific_groups (#7018) …
Modified is_cyclic.exists_monoid_generatorView on Github →
2021-03-17 08:30
src/group_theory/order_of_element.lean
refactor(group_theory/order_of_element): now makes sense for infinite monoids (#6587) …
Modified is_cyclic.exists_monoid_generatorView on Github →
2020-05-12 06:37
src/group_theory/order_of_element.lean
feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623) …
Added is_cyclic.exists_monoid_generatorView on Github →