mem_range_scalar_iff_commute_transvectionStruct

English

A matrix M that commutes with every nontrivial transvection t.toMatrix must be a scalar matrix: M ∈ range(scalar(n)).

Русский

Матрица M, commuting со всеми ненулевыми трансвеκциями, является скалярной матрицей.

LaTeX

$$$\\big(\\forall t:\\text{TransvectionStruct }n\\,R,\\; t.toMatrix \\;\\text{commutes with } M\\big) \\Rightarrow M \\in \\operatorname{range}(\\text{scalar } n)$$$

Lean4

theorem _root_.Matrix.mem_range_scalar_iff_commute_transvectionStruct {M : Matrix n n R} :
    M ∈ Set.range (Matrix.scalar n) ↔ ∀ t : TransvectionStruct n R, Commute t.toMatrix M :=
  by
  refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
  rw [mem_range_scalar_iff_commute_single] at h
  refine (Commute.one_left M).add_left ?_
  convert (h _ _ t.hij).smul_left t.c using 1
  rw [smul_single, smul_eq_mul, mul_one]

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