Commit 2024-03-21 14:51 b6fe43df

View on Github →

chore(LinearAlgebra): fix Fintype/Finite assumptions (#11565) .. in equivOfPiLEquivPi, coePiBasisFun.toMatrix_eq_transpose, vecMul_surjective_iff_exists_left_inverse, and mulVec_surjective_iff_exists_right_inverse

Estimated changes

Modified Mathlib/LinearAlgebra/Determinant.lean

modified def equivOfPiLEquivPi

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

modified theorem Basis.coePiBasisFun.toMatrix_eq_transpose

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

modified theorem Matrix.mulVec_surjective_iff_exists_right_inverse

modified theorem Matrix.mulVec_surjective_iff_isUnit

modified theorem Matrix.mulVec_surjective_of_invertible

modified theorem Matrix.vecMul_surjective_iff_exists_left_inverse

modified theorem Matrix.vecMul_surjective_iff_isUnit

modified theorem Matrix.vecMul_surjective_of_invertible