Theorem Fintype.card_multiplicative
Modification history
2025-03-03 18:20
Mathlib/Algebra/Group/TypeTags/Finite.lean
chore(Algebra/Group): move `Fintype` instances to `TypeTags/Finite.lean` (#21989) …
Modified Fintype.card_multiplicativeView on Github →