Commit 2024-04-18 15:37 e0822742

View on Github →

feat: add Lemma Matrix_toEuclideanLin_apply (#11988) The proposed lemma unfolds the toEuclideanLin definition to express action of a matrix on a vector, without defeq abuse.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem Matrix.piLp_equiv_toEuclideanLin_apply

added theorem Matrix.toEuclideanLin_apply

added theorem Matrix.toEuclideanLin_apply_piLp_equiv_symm