unop_smul_eq_smul — Mathlib

English

If M acts on α and the opposite Mᵐᵒᵖ also acts with IsCentralScalar, then the action of unop m on a equals the action of m on a.

Русский

Если M действует на α и существует противоположность Mᵐᵒᵖ с IsCentralScalar, то действие unop m на a равно действию m на a.

LaTeX

$$$ MulOpposite.unop(m) \cdot a = m \cdot a. $$$

Lean4

@[to_additive]
theorem unop_smul_eq_smul {M α : Type*} [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (m : Mᵐᵒᵖ) (a : α) :
    MulOpposite.unop m • a = m • a := by induction m; exact (IsCentralScalar.op_smul_eq_smul _ a).symm

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