Commit 2024-12-20 05:45 ea22acdd

View on Github →

feat: add bundled multiplication maps for matrices (#19229) This repeats the definitions and theorems about LinearMap.mulLeft and LinearMap.mulRight for rectangular matrices. These definitions (or rather, the continuous versions of them) are needed to state results about Fréchet derivatives of matrices.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Matrix/Basis.lean

modified theorem Matrix.StdBasisMatrix.mul_left_apply_of_ne

modified theorem Matrix.StdBasisMatrix.mul_left_apply_same

modified theorem Matrix.StdBasisMatrix.mul_of_ne

modified theorem Matrix.StdBasisMatrix.mul_right_apply_of_ne

modified theorem Matrix.StdBasisMatrix.mul_right_apply_same

modified theorem Matrix.StdBasisMatrix.mul_same

Created Mathlib/Data/Matrix/Bilinear.lean

added theorem commute_mulLeftLinearMap_mulRightLinearMap

added def mulLeftLinearMap

added theorem mulLeftLinearMap_eq_mulLeft

added theorem mulLeftLinearMap_eq_zero_iff

added theorem mulLeftLinearMap_mul

added theorem mulLeftLinearMap_one

added theorem mulLeftLinearMap_zero_eq_zero

added def mulLinearMap

added theorem mulLinearMap_eq_mul

added def mulRightLinearMap

added theorem mulRightLinearMap_eq_mulRight

added theorem mulRightLinearMap_eq_zero_iff

added theorem mulRightLinearMap_mul

added theorem mulRightLinearMap_one

added theorem mulRightLinearMap_zero_eq_zero

added theorem pow_mulLeftLinearMap

added theorem pow_mulRightLinearMap