eq_of_smul_eq_smul_left — Mathlib

English

In the ring ℤ√d, if a ∈ ℤ with a ≠ 0 and a b = a c, then b = c.

Русский

В кольце ℤ√d, если a ∈ ℤ и a ≠ 0 и a b = a c, то b = c.

LaTeX

$$$a \in \mathbb{Z}, a \neq 0 \Rightarrow a \cdot b = a \cdot c \Rightarrow b = c$$$

Lean4

protected theorem eq_of_smul_eq_smul_left {a : ℤ} {b c : ℤ√d} (ha : a ≠ 0) (h : ↑a * b = a * c) : b = c :=
  by
  rw [Zsqrtd.ext_iff] at h ⊢
  apply And.imp _ _ h <;> simpa only [re_smul, im_smul] using mul_left_cancel₀ ha

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