Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-11-09 12:45
645905bd
View on Github →
chore(InnerProductSpace/Adjoint): isAdjointPair_inner for IsROrC (
#8295
)
Estimated changes
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
modified
theorem
ContinuousLinearMap.isAdjointPair_inner