instIsCentralScalar — Mathlib

English

If SMul R M and SMul Rᵐᵒᵖ M hold, and M has a central scalar action, then ULift M also has a central scalar action.

Русский

Если действии скалярами R и Rᵐᵒᵖ на M совместимы и M имеет центральную скалярную структуру, то ULift M тоже имеет центральную структуру скаляров.

LaTeX

$$IsCentralScalar R (ULift M)$$

Lean4

instance [SMul R M] [SMul Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (ULift M) :=
  ⟨fun r m => congr_arg up <| op_smul_eq_smul r m.down⟩

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