scalar_eq_coe_self_center — Mathlib

English

An element A is central in SL(n,R) if and only if A is a scalar matrix with a scalar r that satisfies r^{card(n)} = 1.

Русский

Элемент A центра в SL(n,R) эквивалентен скалярной матрице с скаляром r, удовлетворяющим r^{|n|}=1.

LaTeX

$$A ∈ center(SL_n(R)) ⇔ ∃ r ∈ R, r^{|n|} = 1 ∧ scalar n r = A$$

Lean4

theorem scalar_eq_coe_self_center (A : center (SpecialLinearGroup n R)) (i : n) :
    scalar n ((A : Matrix n n R) i i) = A :=
  scalar_eq_self_of_mem_center A.property i

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