ofFractionRing_div — Mathlib

English

Division in RatFunc matches division in the fraction ring: ofFractionRing(p/q) = ofFractionRing(p) / ofFractionRing(q).

Русский

Деление в RatFunc совпадает с делением в дробной локализации: ofFractionRing(p/q) = ofFractionRing(p)/ofFractionRing(q).

LaTeX

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

Lean4

theorem ofFractionRing_div (p q : FractionRing K[X]) : ofFractionRing (p / q) = ofFractionRing p / ofFractionRing q :=
  (div_def _ _).symm

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