coe_star — Mathlib

English

For any A in the special unitary group, the projection of star A equals the star of the underlying matrix: (star A).1 = star(A.1).

Русский

Для любого A из группы специальной унитарной верна пропорция: (звезда A).1 = звезда(A.1).

LaTeX

$$$\\forall A \\in \\mathrm{specialUnitaryGroup}(n,\\alpha),\\quad (\\star A).1 = \\star(A.1)$$$

Lean4

@[simp, norm_cast]
theorem coe_star (A : specialUnitaryGroup n α) : (star A).1 = star A.1 :=
  rfl

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