Def LinearMap.IsSymmetric.toSelfAdjoint

Modification history

2023-06-01 13:13

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

feat: port Analysis.InnerProductSpace.Adjoint (#4476)

Added LinearMap.IsSymmetric.toSelfAdjoint View on Github →