Theorem ContinuousLinearMap.isometry_mul_flip

Modification history

2023-08-22 02:46
Mathlib/Analysis/NormedSpace/Star/Unitization.lean
feat: The norm on `Unitization` is a C⋆-norm (#5393) …
Added ContinuousLinearMap.isometry_mul_flipView on Github →