Theorem mul_isometry

Modification history

2023-08-22 02:46
Mathlib/Analysis/NormedSpace/Star/Unitization.lean
feat: The norm on `Unitization` is a C⋆-norm (#5393) …
Deleted mul_isometryView on Github →
2023-05-21 08:32
Mathlib/Analysis/NormedSpace/Star/Mul.lean
feat: port Analysis.NormedSpace.Star.Mul (#4147)
Added mul_isometryView on Github →