Commit 2025-03-03 18:20 1f662d55
View on Github →chore(Algebra/Group): move Fintype
instances to TypeTags/Finite.lean
(#21989)
This change was discussed in the reviews of #21831.
The Fintype
instances on Additive
and Multiplicative
are now found in Algebra.Group.TypeTags.Finite
, alongside the existing Finite
and Infinite
instances. This leaves behind a file containing only a DecidableEq
instance on AddEquiv
/MulEquiv
(which seems not to be used in Mathlib), so I moved the file to Algebra.Group.Equiv.Finite
. I couldn't find an obvious place to put this instance: there seem to be few low-level group theory files that import finiteness.