scalar_commute — Mathlib

English

If r commutes with every element of α, then the scalar matrix scalar n r commutes with any square matrix M.

Русский

Если скаляр r коммутирует со всеми элементами кольца α, то скалярная матрица scalar n r коммутирует с любой квадратной матрицей M.

LaTeX

$$If ∀ r' , Commute r r' then Commute (scalar n r) M$$

Lean4

theorem scalar_commute (r : α) (hr : ∀ r', Commute r r') (M : Matrix n n α) : Commute (scalar n r) M :=
  scalar_comm r hr M

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