mathlib
53128954 - chore(group_theory/order_of_element): move some lemmas (#7031)

Commit
4 years ago
chore(group_theory/order_of_element): move some lemmas (#7031) I moved a few lemmas to `group_theory.subgroup` and to `group_theory.coset` and to `data.finset.basic`. Feel free to suggest different locations if they don't quite fit. This resolves #1563. Renamed `card_trivial` to `subgroup.card_bot` Co-authored-by: Julian-Kuelshammer <68201724+Julian-Kuelshammer@users.noreply.github.com>
Parents
Loading