sub_quot — Mathlib

English

Subtraction in the quotient is induced by subtraction in the base ring: [a] - [b] = [a - b].

Русский

Вычитание в кольце-остатке задаётся через вычитание в исходном кольце: [a] - [b] = [a - b].

LaTeX

$$$[a] - [b] = [a - b]$$$

Lean4

theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
    (⟨Quot.mk _ a⟩ - ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a - b)⟩ :=
  by
  change sub r _ _ = _
  rw [sub_def]
  rfl

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