ofFractionRing_smul — Mathlib

English

Scalar multiplication commutes with the fraction-ring embedding: for any c, ofFractionRing(c • p) = c • ofFractionRing(p).

Русский

Умножение на скаляр бесконечно переносится через отображение в дробную локализацию: ofFractionRing(c • p) = c • ofFractionRing(p).

LaTeX

$$$\forall c\in R,\; \forall p \in \mathrm{FractionRing}(K[X]),\; \operatorname{ofFractionRing}(c \cdot p) = c \cdot \operatorname{ofFractionRing}(p)$$$

Lean4

theorem ofFractionRing_smul [SMul R (FractionRing K[X])] (c : R) (p : FractionRing K[X]) :
    ofFractionRing (c • p) = c • ofFractionRing p :=
  (smul_def _ _).symm

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