det_of_mem_unitary — Mathlib

English

An equivalent formulation: A is in the unitaryGroup if and only if star A · A = 1.

Русский

Эквивалентная формулировка: A в unitaryGroup ⇔ star A · A = 1.

LaTeX

$$$ A \in \mathrm{unitaryGroup}_{n}(\alpha) \iff \star A \; A = 1. $$$

Lean4

theorem det_of_mem_unitary {A : Matrix n n α} (hA : A ∈ Matrix.unitaryGroup n α) : A.det ∈ unitary α :=
  by
  constructor
  · simpa [star, det_transpose] using congr_arg det hA.1
  · simpa [star, det_transpose] using congr_arg det hA.2

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