Commit 2024-02-20 01:19 ea9e243b

View on Github →

chore(LinearAlgebra): Fintype -> Finite (#10722)

Estimated changes

Modified Mathlib/LinearAlgebra/QuadraticForm/IsometryEquiv.lean

Modified Mathlib/LinearAlgebra/StdBasis.lean

modified theorem Matrix.stdBasis_eq_stdBasisMatrix