toFractionRing_smul — Mathlib

English

For RatFunc elements, toFractionRing respects scalar multiplication: toFractionRing(c • p) = c • toFractionRing(p).

Русский

Для элементов RatFunc отображение toFractionRing сохраняет скалярное умножение: toFractionRing(c • p) = c • toFractionRing(p).

LaTeX

$$$\forall c\in R,\; \forall p\in \mathrm{RatFunc}(K),\; \operatorname{toFractionRing}(c \cdot p) = c \cdot \operatorname{toFractionRing}(p)$$$

Lean4

theorem toFractionRing_smul [SMul R (FractionRing K[X])] (c : R) (p : RatFunc K) :
    toFractionRing (c • p) = c • toFractionRing p := by
  cases p
  rw [← ofFractionRing_smul]

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