Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-04 22:22
5ba359da
View on Github →
feat:
H →L[ℂ] H
is a
StarOrderedRing
when
H
is a Hilbert space (
#16462
)
Estimated changes
Modified
Mathlib.lean
Modified
Mathlib/Analysis/InnerProductSpace/Positive.lean
added
theorem
ContinuousLinearMap.antilipschitz_of_forall_le_inner_map
added
theorem
ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map
Created
Mathlib/Analysis/InnerProductSpace/StarOrder.lean
added
theorem
ContinuousLinearMap.IsPositive.spectrumRestricts
added
theorem
ContinuousLinearMap.instStarOrderedRingRCLike