ofFractionRing_mul — Mathlib

English

Multiplication in RatFunc is compatible with multiplication in the fraction ring: the image of the product equals the product of the images.

Русский

Умножение в RatFunc согласуется с умножением в дробной локализации: образ произведения равен произведению образов.

LaTeX

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

Lean4

theorem ofFractionRing_mul (p q : FractionRing K[X]) : ofFractionRing (p * q) = ofFractionRing p * ofFractionRing q :=
  (mul_def _ _).symm

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