eq_of_forall_dvd — Mathlib

English

Let α be a CancelCommMonoidWithZero. If for every element c of α we have a divides c if and only if b divides c, then a equals b. (The unit group is subsingleton in this context.)

Русский

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

LaTeX

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

Lean4

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

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