Commit 2025-03-03 18:20 1f662d55

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.