norm_coe_unitary_mul — Mathlib

English

For a unitary U and any A ∈ E, ∥(U) A∥ = ∥A∥.

Русский

Для унитарного элемента U и любого A ∈ E верно ∥(U) A∥ = ∥A∥.

LaTeX

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

Lean4

@[simp]
theorem norm_coe_unitary_mul (U : unitary E) (A : E) : ‖(U : E) * A‖ = ‖A‖ :=
  by
  nontriviality E
  refine le_antisymm ?_ ?_
  ·
    calc
      _ ≤ ‖(U : E)‖ * ‖A‖ := norm_mul_le _ _
      _ = ‖A‖ := by rw [norm_coe_unitary, one_mul]
  ·
    calc
      _ = ‖(U : E)⋆ * U * A‖ := by rw [unitary.coe_star_mul_self U, one_mul]
      _ ≤ ‖(U : E)⋆‖ * ‖(U : E) * A‖ := by
        rw [mul_assoc]
        exact norm_mul_le _ _
      _ = ‖(U : E) * A‖ := by rw [norm_star, norm_coe_unitary, one_mul]

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