instDistribMulActionOfIsScalarTower

English

There is a lifted DistribMulAction on Ore localization via scalar towers.

Русский

Существует перенесённое DistribMulAction на локализацию Оре через скалярные башни.

LaTeX

$$IsScalarTower (R0, R, X) ⇒ DistribMulAction R0 (OreLocalization S X)$$

Lean4

instance {R₀} [Monoid R₀] [MulAction R₀ X] [MulAction R₀ R] [IsScalarTower R₀ R X] [IsScalarTower R₀ R R] :
    DistribMulAction R₀ X[S⁻¹]
    where
  smul_zero _ := by rw [← smul_one_oreDiv_one_smul, smul_zero]
  smul_add _ _ _ := by simp only [← smul_one_oreDiv_one_smul, smul_add]

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