op_smul_one_eq_diagonal — Mathlib

English

For any a ∈ α, the left action of MulOpposite.op(a) on the identity matrix equals the diagonal diag(a).

Русский

Для любого a ∈ α левое действие MulOpposite.op(a) на единичную матрицу равно диагональной diag(a).

LaTeX

$$$ \\operatorname{MulOpposite}.op(a) \\cdot I = \\operatorname{diagonal}(a) $$$

Lean4

theorem op_smul_one_eq_diagonal [DecidableEq m] (a : α) : MulOpposite.op a • (1 : Matrix m m α) = diagonal fun _ => a :=
  by simp_rw [← diagonal_one, ← diagonal_smul, Pi.smul_def, op_smul_eq_mul, one_mul]

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