Commit 2024-04-21 11:20 a7a70332

View on Github →

chore(SpecificGroups/Cyclic): Fintype -> Finite (#12299)

Estimated changes

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

deleted theorem IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype

added theorem isCyclic_iff_exists_ofOrder_eq_natCard