mem_range_scalar_iff_commute_single'

English

For matrices over a semiring, the center equals the image of the scalar matrices under the scalar map.

Русский

Для матриц над полус кольцом центр равен изображению скалярных матриц через скалярное отображение.

LaTeX

$$$$\\mathrm{Subsemiring}.\\mathrm{center}(\\\\mathrm{Matrix}(n,n,\\\\alpha)) = \\mathrm{Subsemiring}.\\mathrm{map}(\\\\mathrm{Matrix}.\\\\mathrm{scalar}(n)).$$$$

Lean4

/-- `M` is a scalar matrix if and only if it commutes with every `single`. -/
theorem mem_range_scalar_iff_commute_single' {M : Matrix n n α} :
    M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), Commute (single i j 1) M :=
  by
  refine
    ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_, fun hM => mem_range_scalar_iff_commute_single.mpr <| fun i j _ => hM i j⟩
  rw [scalar_commute_iff]
  simp

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