instSMulCauchyOfIsScalarTower — Mathlib

English

If γ acts on β and IsScalarTower holds, then there is a compatible scalar action on the completion: c • mk f = mk (c • f).

Русский

Пусть γ действует на β и выполняется IsScalarTower; тогда на завершении есть совместное действие скаляров: c • mk f = mk (c • f).

LaTeX

$$$\text{For } \gamma:\, \gamma \to \beta,\; c\,\operatorname{mk} f = \operatorname{mk}(c\,f)$$$

Lean4

instance {γ : Type*} [SMul γ β] [IsScalarTower γ β β] : SMul γ (Cauchy abv) :=
  ⟨fun c => (Quotient.map (c • ·)) fun _ _ hf => smul_equiv_smul _ hf⟩

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