mathlib3
ac49df81 - feat(group_theory/exponent): `card G ∣ exponent G ^ rank G` (#16354)

Commit

3 years ago

feat(group_theory/exponent): `card G ∣ exponent G ^ rank G` (#16354) This PR adds a lemma stating that `nat.card G ∣ monoid.exponent G ^ group.rank G`.

Author

tb65536

Parents

3c139aa9

mathlib3 ac49df81 - feat(group_theory/exponent): `card G ∣ exponent G ^ rank G` (#16354)

mathlib3
ac49df81 - feat(group_theory/exponent): `card G ∣ exponent G ^ rank G` (#16354)