Commit 2026-02-11 11:08 1a8f46e1

View on Github →

chore: fix Fintype instances that are not used for data in types (#35102) If a theorem has a Fintype instance which is only used in proofs in the remainder of the theorem's type, it can be replaced with Finite. These were found by the upgrade to the unused instances in types linter in #32440.

Estimated changes

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

Modified Mathlib/Analysis/BoxIntegral/UnitPartition.lean

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified theorem LinearMap.toMatrix_smulRight

modified theorem LinearMap.toMatrix_toSpanSingleton

modified theorem Matrix.toLin_apply

modified theorem Matrix.toLin_apply_eq_zero_iff

modified theorem Matrix.toLin_self

Modified Mathlib/LinearAlgebra/Multilinear/Basis.lean

Modified Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean

modified theorem IsIntegralClosure.range_le_span_dualBasis

modified theorem integralClosure_le_span_dualBasis

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean

Modified Mathlib/Topology/Algebra/Module/FiniteDimension.lean