scalar_eq_self_of_mem_center — Mathlib

English

If A is central, then ∃ r with A = scalar n r and the equation on the diagonal entries holds: scalar n (A_{ii}) = A.

Русский

Если A лежит в центре, то существует скаляр r, такой что A = scalar n r, и диагональные элементы задают A.

LaTeX

$$scalar n (A_{ii}) = A$$

Lean4

theorem scalar_eq_self_of_mem_center {A : SpecialLinearGroup n R} (hA : A ∈ center (SpecialLinearGroup n R)) (i : n) :
    scalar n (A i i) = A :=
  by
  obtain ⟨r : R, hr : scalar n r = A⟩ :=
    mem_range_scalar_of_commute_transvectionStruct fun t ↦
      Subtype.ext_iff.mp <| Subgroup.mem_center_iff.mp hA ⟨t.toMatrix, by simp⟩
  simp [← congr_fun₂ hr i i, ← hr]

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