Commit 2023-07-13 08:07 350feed7

View on Github →

feat(GroupTheory/Sylow): add inverse to card_eq_multiplicity (#5831) Port https://github.com/leanprover-community/mathlib/pull/18300 to mathlib4

Estimated changes

added theorem Sylow.coe_ofCard
added def Sylow.ofCard