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]