Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-06-03 01:29
efe888f2
View on Github →
chore(Analysis/InnerProductSpace): make
adjointAux
private (
#40091
)
Estimated changes
Modified
Mathlib/Analysis/InnerProductSpace/Adjoint.lean
added
def
ContinuousLinearMap.adjointAux