Commit 2024-03-18 10:51 e22cf367

View on Github →

chore(*): Fintype -> Finite, drop Decidable (#11423) Also, in some cases drop unneeded Fintype arguments.

Estimated changes

Modified Mathlib/Algebra/Module/Zlattice.lean

modified theorem Zspan.discreteTopology_pi_basisFun

Modified Mathlib/Data/Matrix/Basic.lean

modified theorem Matrix.diagonal_neg

modified theorem Matrix.diagonal_smul

modified theorem Matrix.op_smul_one_eq_diagonal

modified theorem Matrix.smul_one_eq_diagonal

Modified Mathlib/Data/Matrix/Basis.lean

Modified Mathlib/Data/Matrix/DMatrix.lean

modified def DMatrix

Modified Mathlib/Geometry/Manifold/ChartedSpace.lean

modified theorem piChartedSpace_chartAt

Modified Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean