sub_def — Mathlib

English

Subtraction in RatFunc is compatible with the fraction-ring subtraction, mirroring the additive structure.

Русский

В RatFunc вычитание согласуется с вычитанием в дробной локализации, сохраняется структура сложения.

LaTeX

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

Lean4

theorem sub_def : eta_helper Eq✝ @sub.{} @(delta% @definition✝) :=
  by
  intros
  delta sub
  rw [show wrapped✝ = ⟨@definition✝.{}, rfl✝⟩ from Subtype.ext✝ wrapped✝.2.symm✝]
  rfl

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