Theorem OrthonormalBasis.toMatrix_orthonormalBasis_self_mul_conjTranspose

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_self_mul_conjTransposeView on Github →