op_smul_eq_mul_diagonal — Mathlib

English

For any matrix M and scalar a, the left action of a via the opposite algebra on M equals the left-multiplication by a diagonal diag(a) on the right: (MulOpposite.op a) · M = M · diag(a).

Русский

Пусть M — матрица и a — скаляр. Тогда левое действие a через противоположную алгебру на M равно левому умножению на diag(a) справа: MulOpposite.op(a) · M = M · diag(a).

LaTeX

$$$ (\\mathrm{MulOpposite}.op\\,a) \\cdot M = M \\cdot \\operatorname{diagonal}(a) $$$

Lean4

theorem op_smul_eq_mul_diagonal [Fintype n] [DecidableEq n] (M : Matrix m n α) (a : α) :
    MulOpposite.op a • M = M * (diagonal fun _ : n => a) :=
  by
  ext
  simp

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