eq_zero_of_zero_dvd

Mathlib.Algebra.GroupWithZero.Divisibility

URI: https://scilib.ai/kg/mathlib#eq_zero_of_zero_dvd

English

If 0 divides a in a semigroup with zero and no zero divisors, then a = 0.

Русский

Если 0 делит a в полугруппе с нулём и отсутствии нулевых делителей, то a = 0.

LaTeX

$$0 \mid a \Rightarrow a = 0$$

Lean4

theorem eq_zero_of_zero_dvd (h : 0 ∣ a) : a = 0 :=
  Dvd.elim h fun c H' => H'.trans (zero_mul c)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru