Theorem LinearMap.isAdjointPair_inner

Modification history

2023-11-10 12:09
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
chore(Analysis/InnerProductSpace): LinearMap.isAdjointPair_inner generalization to isROrC (#8309) …
Modified LinearMap.isAdjointPair_innerView on Github →
2023-06-01 13:13
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
feat: port Analysis.InnerProductSpace.Adjoint (#4476)
Added LinearMap.isAdjointPair_innerView on Github →