Commit 2023-08-16 23:07 ae74c2e5

View on Github →

feat: star self dot product eq zero and kernel lemmas apply to matrices not just vectors (#6587) This generalizes two results about vectors to matrices:

dotProduct_star_self_eq_zero to conjTranspose_mul_self_eq_zero
dotProduct_self_star_eq_zero to self_mul_conjTranspose_eq_zero It also adds lemmas linking the kernel (under left-multiplication, right-multiplication, vecMul, and mulVec) of $A$, $A^HA$, and $AA^H$. Some of these lemmas are used in the SVD decomposition theorem of R or C matrices #6042

Estimated changes

Modified Mathlib/Data/Matrix/Rank.lean

Modified Mathlib/LinearAlgebra/Matrix/DotProduct.lean

added theorem Matrix.conjTranspose_mul_self_eq_zero

added theorem Matrix.conjTranspose_mul_self_mulVec_eq_zero

added theorem Matrix.conjTranspose_mul_self_mul_eq_zero

modified theorem Matrix.dotProduct_self_star_eq_zero

modified theorem Matrix.dotProduct_star_self_eq_zero

added theorem Matrix.mul_conjTranspose_mul_self_eq_zero

added theorem Matrix.mul_self_mul_conjTranspose_eq_zero

added theorem Matrix.self_mul_conjTranspose_eq_zero

added theorem Matrix.self_mul_conjTranspose_mulVec_eq_zero

added theorem Matrix.self_mul_conjTranspose_mul_eq_zero

added theorem Matrix.vecMul_conjTranspose_mul_self_eq_zero

added theorem Matrix.vecMul_self_mul_conjTranspose_eq_zero