instModuleOfIsScalarTower — Mathlib

English

Assuming a scalar tower R0 → R → X, OreLocalization S X is a module over R0 with compatible actions.

Русский

При предположении тензорной башни R0 → R → X локализация Ore X[S^{-1}] является модулем над R0 с согласованными действиями.

LaTeX

$$Module R0 (OreLocalization S X)$$

Lean4

instance {R₀} [Semiring R₀] [Module R₀ X] [Module R₀ R] [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] : Module R₀ X[S⁻¹]
    where
  add_smul r s x := by simp only [← smul_one_oreDiv_one_smul, add_smul, ← add_oreDiv]
  zero_smul x := by rw [← smul_one_oreDiv_one_smul, zero_smul, zero_oreDiv, zero_smul]

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