add_comm — Mathlib

English

Addition on the Ore localization is commutative: x + y = y + x when X is AddCommMonoid.

Русский

Сложение на локализации Оре коммутативно: x + y = y + x при X это AddCommMonoid.

LaTeX

$$x + y = y + x$$

Lean4

protected theorem add_comm (x y : X[S⁻¹]) : x + y = y + x :=
  by
  induction x with
  | _ r s
  induction y with
  | _ r' s'
  rcases oreDivAddChar' r r' s s' with ⟨ra, sa, ha, ha'⟩
  rw [ha', oreDiv_add_char' s' s _ _ ha.symm (ha ▸ (sa * s).2), add_comm]
  congr; ext; exact ha

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