Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-10-15 15:12 c5930f57

View on Github →

feat(group_theory.order_of_element): subgroups of cyclic groups are cyclic (#423)

feat(group_theory.order_of_element): subgroups of cyclic groups are cyclic
delete new line

Estimated changes

Modified group_theory/order_of_element.lean

Modified group_theory/subgroup.lean

added theorem is_add_subgroup.gsmul_coe

added theorem is_subgroup.coe_gpow

added theorem is_subgroup.coe_inv

Modified group_theory/submonoid.lean

added theorem is_add_submonoid.smul_coe

added theorem is_submonoid.coe_mul

added theorem is_submonoid.coe_one

added theorem is_submonoid.coe_pow