norm_mul_coe_unitary — Mathlib

English

For A ∈ E and unitary U ∈ E, ∥A U∥ = ∥A∥.

Русский

Для A ∈ E и унитарного U ∈ E выполняется ∥A U∥ = ∥A∥.

LaTeX

$$$ \| A \cdot (U : E) \| = \|A\| $$$

Lean4

@[simp]
theorem norm_mul_coe_unitary (A : E) (U : unitary E) : ‖A * U‖ = ‖A‖ :=
  calc
    _ = ‖((U : E)⋆ * A⋆)⋆‖ := by simp only [star_star, star_mul]
    _ = ‖(U : E)⋆ * A⋆‖ := by rw [norm_star]
    _ = ‖A⋆‖ := (norm_mem_unitary_mul (star A) (unitary.star_mem U.prop))
    _ = ‖A‖ := norm_star _

Похожие утверждения