ofFractionRing_add — Mathlib

English

The same additive compatibility holds for two fractional ring elements p and q: ofFractionRing(p+q) = ofFractionRing(p) + ofFractionRing(q).

Русский

Сохранение сложения для элементов дробной локализации: 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_add (p q : FractionRing K[X]) : ofFractionRing (p + q) = ofFractionRing p + ofFractionRing q :=
  (add_def _ _).symm

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