add_left_cancel_of_ne_top — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem add_left_cancel_of_ne_top {x y z : ArchimedeanClass R} (hx : x ≠ ⊤) (h : x + y = x + z) : y = z :=
  by
  induction x with
  | mk x
  induction y with
  | mk y
  induction z with
  | mk z
  simp_rw [← mk_mul, mk_eq_mk] at h
  obtain ⟨⟨m, hm⟩, ⟨n, hn⟩⟩ := h
  simp_rw [abs_mul, mul_comm |x|, nsmul_eq_mul, ← mul_assoc, ← nsmul_eq_mul] at hm hn
  refine mk_eq_mk.2 ⟨⟨m, ?_⟩, ⟨n, ?_⟩⟩ <;> exact le_of_mul_le_mul_right ‹_› (by simpa using hx)

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