Theorem Unitization.norm_splitMul_snd_sq

Modification history

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