isScalarTower — Mathlib

English

There is a compatible scalar tower making AddGroupSeminorm into a module over multiple scalar rings, i.e., the defined tower laws hold.

Русский

Существуют совместимости тензорной цепи скаляров, делающие AddGroupSeminorm модулем над несколькими кольцами скаляров.

LaTeX

$$$\text{IsScalarTower } R R' (\text{AddGroupSeminorm } E)$$$

Lean4

instance isScalarTower [SMul R' ℝ] [SMul R' ℝ≥0] [IsScalarTower R' ℝ≥0 ℝ] [SMul R R'] [IsScalarTower R R' ℝ] :
    IsScalarTower R R' (AddGroupSeminorm E) :=
  ⟨fun r a p => ext fun x => smul_assoc r a (p x)⟩

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