zero

Mathlib.Algebra.Ring.Parity

URI: https://scilib.ai/kg/mathlib#IsSquare.zero

English

In any semiring, 0 is a square: there exists x with x^2 = 0.

Русский

В любом полукольце ноль является квадратом: существует x, такое что x^2 = 0.

LaTeX

$$$\exists x \in \alpha,\ x^2 = 0$$$

Lean4

@[simp]
theorem zero [MulZeroClass α] : IsSquare (0 : α) :=
  ⟨0, (mul_zero _).symm⟩

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

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

Разделы

Аффилиация

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