eq_of_forall_dvd' — Mathlib

English

Let α be CancelCommMonoidWithZero with Subsingleton of units. If for every c in α we have c divides a iff c divides b, then a = b.

Русский

Пусть α — CancelCommMonoidWithZero, причём множество единиц остается тривиальным. Если для каждого c из α верно c делит a тогда и только тогда, когда c делит b, то a = b.

LaTeX

$$$\\forall c:\\alpha\\, (c \\mid a \\iff c \\mid b) \\Rightarrow a = b$$$

Lean4

theorem eq_of_forall_dvd' (h : ∀ c, c ∣ a ↔ c ∣ b) : a = b :=
  ((h _).1 dvd_rfl).antisymm <| (h _).2 dvd_rfl

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