Theorem OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_self

Modification history

2024-09-25 19:13
Mathlib/Analysis/InnerProductSpace/PiL2.lean
feat: `Mᴴ * M = 1` when `M := a.toBasis.toMatrix b` (#17136) …
Added OrthonormalBasis.toMatrix_orthonormalBasis_conjTranspose_mul_selfView on Github →