English
There is a StarHomClass instance for WeakDual.Complex, making its morphisms star-preserving maps into the Complex numbers.
Русский
Существует экземпляр StarHomClass для WeakDual.Complex, обеспечивающий сохранение звезды в отображениях к Complex.
LaTeX
$$$\text{WeakDual.Complex.instStarHomClass : StarHomClass (WeakDual.Complex) A \mathbb{C}$$$
Lean4
theorem opNorm_mul_flip_apply (a : E) : ‖(mul 𝕜 E).flip a‖ = ‖a‖ :=
by
refine le_antisymm (opNorm_le_bound _ (norm_nonneg _) fun b => by simpa only [mul_comm] using norm_mul_le b a) ?_
suffices ‖mul 𝕜 E (star a)‖ ≤ ‖(mul 𝕜 E).flip a‖ by simpa only [ge_iff_le, opNorm_mul_apply, norm_star] using this
refine opNorm_le_bound _ (norm_nonneg _) fun b => ?_
calc
‖mul 𝕜 E (star a) b‖ = ‖(mul 𝕜 E).flip a (star b)‖ := by
simpa only [mul_apply', flip_apply, star_mul, star_star] using norm_star (star b * a)
_ ≤ ‖(mul 𝕜 E).flip a‖ * ‖b‖ := by
simpa only [flip_apply, mul_apply', norm_star] using le_opNorm ((mul 𝕜 E).flip a) (star b)
