op_smul_eq_op_smul_op — Mathlib

English

For SMul M α and SMul Mᵐᵒᵖ α with IsCentralScalar M α, the equality op(r • a) = op(r) • op(a) holds.

Русский

Пусть есть действия SMul M α и SMul Mᵐᵒᵖ α с IsCentralScalar M α; тогда выполняется равенство op(r • a) = op(r) • op(a).

LaTeX

$$$\forall r\in M, a\in α:\; op(r \cdot a) = op(r) \cdot op(a)$$$

Lean4

@[to_additive]
theorem op_smul_eq_op_smul_op [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α) :
    op (r • a) = op r • op a :=
  (op_smul_eq_smul r (op a)).symm

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