Commit 2024-09-25 19:13 15dec280

View on Github →

feat: Mᴴ * M = 1 when M := a.toBasis.toMatrix b (#17136) This partially generalizes an existing result to work when the indices are different.

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

added theorem OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self

added theorem OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose

Modified Mathlib/Data/Matrix/ColumnRowPartitioned.lean

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

added theorem Matrix.mul_eq_one_comm_of_equiv