Theorem ContinuousLinearMap.isUnit_of_forall_le_norm_inner_map

Modification history

2024-09-04 22:22
Mathlib/Analysis/InnerProductSpace/Positive.lean
feat: `H →L[ℂ] H` is a `StarOrderedRing` when `H` is a Hilbert space (#16462)
Added ContinuousLinearMap.isUnit_of_forall_le_norm_inner_mapView on Github →