Commit 2024-03-21 09:38 aab5a051

View on Github →

chore(AffineSpace/Matrix): fix Fintype/Finite (#11559)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/Matrix.lean

modified theorem AffineBasis.affineIndependent_of_toMatrix_right_inv

modified theorem AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv

modified theorem AffineBasis.toMatrix_row_sum_one