Theorem ContinuousLinearMap.isAdjointPair_inner

Modification history

2023-11-09 12:45

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

chore(InnerProductSpace/Adjoint): isAdjointPair_inner for IsROrC (#8295)

Modified ContinuousLinearMap.isAdjointPair_inner View on Github →

2023-06-01 13:13

Mathlib/Analysis/InnerProductSpace/Adjoint.lean

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

Added ContinuousLinearMap.isAdjointPair_inner View on Github →