zero_ne_mul_self

Mathlib.Algebra.GroupWithZero.Defs

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

English

0 is not equal to a^2 unless a = 0; equivalently, a^2 ≠ 0 iff a ≠ 0.

Русский

0 не равен a^2, если только a ≠ 0; иначе a^2 ≡ 0.

LaTeX

$$0 \neq a^2 \iff a \neq 0$$

Lean4

theorem zero_ne_mul_self : 0 ≠ a * a ↔ a ≠ 0 :=
  zero_eq_mul_self.not

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

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

Разделы

Аффилиация

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