Commit 2024-04-07 05:06 562a9a45

View on Github →

chore(Matrix/ToLin): fix Fintype/Finite (#11734) Also drop a no longer needed [DecidableEq _] argument in 1 lemma. It was needed to generate a computable Fintype (Set.range _) instance but a Finite instance doesn't need it.

Estimated changes

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Data/Matrix/Rank.lean

modified theorem Matrix.rank_diagonal

modified theorem Matrix.rank_eq_finrank_range_toLin

modified theorem Matrix.rank_le_card_height

modified theorem Matrix.rank_mul_eq_right_of_isUnit_det

modified theorem Matrix.rank_mul_le_right

Modified Mathlib/LinearAlgebra/Contraction.lean

modified theorem toMatrix_dualTensorHom

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

modified theorem Basis.toLin_toMatrix

modified theorem LinearMap.toMatrix_id_eq_basis_toMatrix

modified theorem basis_toMatrix_mul

modified theorem basis_toMatrix_mul_linearMap_toMatrix

modified theorem basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix

modified theorem linearMap_toMatrix_mul_basis_toMatrix

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified theorem LinearMap.toMatrix_comp

modified theorem LinearMap.toMatrix_reindexRange

modified theorem Matrix.toLin_mul

modified theorem Matrix.toLin_mul_apply

Modified Mathlib/LinearAlgebra/TensorProduct/Matrix.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean