ofFractionRing_neg — Mathlib

English

The image of negation under the fraction-ring map equals the negation of the image: ofFractionRing(-p) = -ofFractionRing(p).

Русский

Образ отрицания в дробной локализации равен отрицанию образа: ofFractionRing(-p) = -ofFractionRing(p).

LaTeX

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

Lean4

theorem ofFractionRing_neg (p : FractionRing K[X]) : ofFractionRing (-p) = -ofFractionRing p :=
  (neg_def _).symm

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