instIsScalarTower — Mathlib

English

If M,N act on X with UniformContinuousConstSMul and IsScalarTower M N X, then IsScalarTower M N (Completion X).

Русский

Если M, N действуют на X с равномерно непрерывным умножением констант и существует IsScalarTower M N X, то IsScalarTower M N (Completion X).

LaTeX

$$$IsScalarTower\\ M\\ N\\ (Completion\\ X)$$$

Lean4

@[to_additive]
instance instIsScalarTower [SMul N X] [SMul M N] [UniformContinuousConstSMul M X] [UniformContinuousConstSMul N X]
    [IsScalarTower M N X] : IsScalarTower M N (Completion X) :=
  ⟨fun m n x =>
    by
    have : _ = (_ : Completion X → Completion X) :=
      map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)
    refine Eq.trans ?_ (congr_fun this.symm x)
    exact congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))⟩

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