Commit 2024-02-14 18:23 aa79ce07

View on Github →

chore(OrderOfElement,Sylow): Fintype -> Finite (#10550)

Estimated changes

Modified Mathlib/GroupTheory/OrderOfElement.lean

modified def subgroupOfIdempotent

modified def submonoidOfIdempotent

Modified Mathlib/GroupTheory/Sylow.lean