Commit 2024-01-06 09:51 f20d8884

View on Github →

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

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Adjoint.lean

added def LinearMap.toMatrixOrthonormal

added theorem LinearMap.toMatrix_adjoint

modified theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint

added theorem Matrix.toLin_conjTranspose