Def ContinuousLinearMap.adjoint

Modification history

2023-06-01 13:13

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

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

Added ContinuousLinearMap.adjoint View on Github →