scalar_commute_iff — Mathlib

English

For a square matrix M and a scalar r, Commute (scalar n r) M holds if and only if r acts on M by the left exactly as MulOpposite.op r acts on M from the right.

Русский

Для квадратной матрицы M и скаляра r выполняется эквивалентно: скалярная матрица слева по r коммутирует с M тогда и только тогда, когда левостороннее действие r на M совпадает с правым действием MulOpposite r.

LaTeX

$$Commute (scalar n r) M \iff r \cdot M = MulOpposite.op(r) \cdot M$$

Lean4

theorem scalar_commute_iff {r : α} {M : Matrix n n α} : Commute (scalar n r) M ↔ r • M = MulOpposite.op r • M :=
  scalar_comm_iff

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