Def LinearMap.toMatrixOrthonormal

Modification history

2024-01-06 09:51

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

feat: relate `Matrix.conjTranspose` to `LinearMap.adjoint` (#9471)

Added LinearMap.toMatrixOrthonormal View on Github →