ofFractionRing_sub — Mathlib

English

Subtraction in the fractional context corresponds to subtraction in RatFunc, mirroring the H-substructure.

Русский

Расширение в FractionRing сохраняет операцию деления (вычитание) в RatFunc, согласуя структуру.

LaTeX

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

Lean4

theorem ofFractionRing_sub (p q : FractionRing K[X]) : ofFractionRing (p - q) = ofFractionRing p - ofFractionRing q :=
  (sub_def _ _).symm

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