instIsScalarTowerInteger — Mathlib

English

There is a compatible scalar multiplication between the integer subrings of vR and vA that respects the valuation.

Русский

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

LaTeX

$$$ \\text{val\_smul }(r\\in vR.integer)(a\\in vA.integer) = \\text{the same product in the ambient rings}$$$

Lean4

instance instIsScalarTowerInteger : IsScalarTower vR.integer vA.integer A where
  smul_assoc x y
    z := by
    simp only [Algebra.smul_def]
    exact mul_assoc _ _ _

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