instIsCentralScalar — Mathlib

English

If each fiber α_i has a central scalar action of M and similarly for β, then Sum α β has a central scalar action of M.

Русский

Если для каждого i α_i имеет центральное скалярное действие M, и аналогично для β, то Sum α β имеет центральное скалярное действие M.

LaTeX

$$$[\forall i, IsCentralScalar M α_i][IsCentralScalar M β] \Rightarrow IsCentralScalar M (Sum α β).$$$

Lean4

@[to_additive]
instance [SMul Mᵐᵒᵖ α] [SMul Mᵐᵒᵖ β] [IsCentralScalar M α] [IsCentralScalar M β] : IsCentralScalar M (α ⊕ β) :=
  ⟨fun a x => by
    cases x
    exacts [congr_arg inl (op_smul_eq_smul _ _), congr_arg inr (op_smul_eq_smul _ _)]⟩

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