eq_zero_or_neZero

Mathlib.Algebra.NeZero

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

English

For any a, either a = 0 or NeZero a holds.

Русский

Для любого элемента a либо a = 0, либо выполняется NeZero a.

LaTeX

$$$ a = 0 \lor \mathrm{NeZero}(a) $$$

Lean4

theorem eq_zero_or_neZero (a : R) : a = 0 ∨ NeZero a :=
  (eq_or_ne a 0).imp_right NeZero.mk

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

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

Разделы

Аффилиация

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