instIsCentralScalar — Mathlib

English

If each fiber α_i admits a central scalar action of M (IsCentralScalar M (α_i)) then the Σ-type Σ i, α_i also has a central scalar action of M.

Русский

Если на каждом слое α_i действует центрированное скалярное действие M, то Σ i, α_i тоже имеет центрированное скалярное действие M.

LaTeX

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

Lean4

@[to_additive]
instance [∀ i, SMul Mᵐᵒᵖ (α i)] [∀ i, IsCentralScalar M (α i)] : IsCentralScalar M (Σ i, α i) :=
  ⟨fun a x => by
    cases x
    rw [smul_mk, smul_mk, op_smul_eq_smul]⟩

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