instIsScalarTower — Mathlib

English

There is a canonical IsScalarTower for the base scalars R and the localized scalars; the scalar action is compatible with the Ore localization structure.

Русский

Существует канонический IsScalarTower для базовых скаляров R и локализованных скаляров; действие скаляров совместимо со структурой локализации Ора.

LaTeX

$$$\\text{IsScalarTower}(R,\,R',\,X[S^{-1}])$ with the expected compatibility axioms.$$

Lean4

@[to_additive]
instance : IsScalarTower R R' X[S⁻¹] where
  smul_assoc r m
    x :=
    by
    rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, ← mul_smul, mul_div_one]
    simp only [smul_mul_assoc, smul_assoc, one_mul]

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