Theorem Matrix.toEuclideanLin_conjTranspose_eq_adjoint

Modification history

2024-01-06 09:51
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat: relate `Matrix.conjTranspose` to `LinearMap.adjoint` (#9471)
Modified Matrix.toEuclideanLin_conjTranspose_eq_adjointView on Github →
2023-06-01 13:13
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat: port Analysis.InnerProductSpace.Adjoint (#4476)
Added Matrix.toEuclideanLin_conjTranspose_eq_adjointView on Github →