star_coe_unitarySelfAddISMul — Mathlib

English

For a selfadjoint element a, star of the unitarySelfAddISMul a is a minus i times the square root expression: star(unitarySelfAddISMul a) = a − i sqrt(1 − a^2).

Русский

Для самоприводимого элемента a выполняется: звезда(unitarySelfAddISMul a) = a − i sqrt(1 − a^2).

LaTeX

$$$\operatorname{star}\big(\text{unitarySelfAddISMul } a \big) = a - i \sqrt{1 - a^2}$$$

Lean4

theorem star_coe_unitarySelfAddISMul (a : selfAdjoint A) (ha_norm : ‖a‖ ≤ 1) :
    (star (unitarySelfAddISMul a ha_norm) : A) = a - I • CFC.sqrt (1 - a ^ 2 : A) := by
  simp [IsSelfAdjoint.star_eq, ← sub_eq_add_neg, (CFC.sqrt_nonneg (1 - a ^ 2 : A)).isSelfAdjoint]

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