add_right_cancel_of_ne_top — Mathlib

English

In ArchimedeanClass over a linear ordered ring, if x ≠ ⊤ and y + x = z + x, then y = z.

Русский

В ArchimedeanClass над линейно упорядоченным кольцом, если x ≠ ⊤ и y + x = z + x, то y = z.

LaTeX

$$$\forall x,y,z \in \operatorname{ArchimedeanClass}(R),\ x \neq \top \rightarrow y+x = z+x \rightarrow y=z.$$$

Lean4

theorem add_right_cancel_of_ne_top {x y z : ArchimedeanClass R} (hx : x ≠ ⊤) (h : y + x = z + x) : y = z :=
  by
  simp_rw [← add_comm x] at h
  exact add_left_cancel_of_ne_top hx h

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