Commit 2023-05-03 06:27 2d975554

View on Github →

feat: port LinearAlgebra.AffineSpace.Matrix (#3775)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/AffineSpace/Matrix.lean

added theorem AffineBasis.affineIndependent_of_toMatrix_right_inv

added theorem AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv

added theorem AffineBasis.det_smul_coords_eq_cramer_coords

added theorem AffineBasis.isUnit_toMatrix

added theorem AffineBasis.isUnit_toMatrix_iff

added theorem AffineBasis.toMatrix_apply

added theorem AffineBasis.toMatrix_inv_vecMul_toMatrix

added theorem AffineBasis.toMatrix_mul_toMatrix

added theorem AffineBasis.toMatrix_row_sum_one

added theorem AffineBasis.toMatrix_self

added theorem AffineBasis.toMatrix_vecMul_coords