unop_smul_eq_unop_smul_unop — Mathlib

English

If M acts on α and αᵐᵒᵖ is involved, then unop(r • a) = unop r • unop a for r ∈ Mᵐᵒᵖ and a ∈ αᵐᵒᵖ.

Русский

Если есть действие M на α и рассматривается αᵐᵒᵖ, то unop(r • a) = unop r • unop a для r ∈ Mᵐᵒᵖ, a ∈ αᵐᵒᵖ.

LaTeX

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

Lean4

@[to_additive]
theorem unop_smul_eq_unop_smul_unop [SMul M α] [SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : Mᵐᵒᵖ) (a : αᵐᵒᵖ) :
    unop (r • a) = unop r • unop a :=
  (unop_smul_eq_smul r (unop a)).symm

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