instIsCentralScalar — Mathlib

English

There is a central scalar structure on the Ore localization, i.e., scalars from the opposite of R act centrally with respect to the localization.

Русский

Существует центральная структура скаляров на локализации Ора: скаляры из R^{op} действуют центрально относительно локализации.

LaTeX

$$$\\text{IsCentralScalar}(R,X[S^{-1}]).$$$

Lean4

@[to_additive]
instance [SMul Rᵐᵒᵖ M] [SMul Rᵐᵒᵖ X] [IsScalarTower Rᵐᵒᵖ M M] [IsScalarTower Rᵐᵒᵖ M X] [IsCentralScalar R M] :
    IsCentralScalar R X[S⁻¹] where
  op_smul_eq_smul r x := by rw [← smul_one_oreDiv_one_smul, ← smul_one_oreDiv_one_smul, op_smul_eq_smul]

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