zero_eq_mul_self

Mathlib.Algebra.GroupWithZero.Defs

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

English

0 equals a^2 if and only if a = 0.

Русский

0 равно a^2 тогда и только тогда, когда a = 0.

LaTeX

$$0 = a^2 \iff a = 0$$

Lean4

theorem zero_eq_mul_self : 0 = a * a ↔ a = 0 := by simp

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

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

Разделы

Аффилиация

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