neg_eq_self_iff

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#SignType.neg_eq_self_iff

English

An element -a equals a if and only if a = 0.

Русский

Элемент -a равен a тогда и только тогда, когда a = 0.

LaTeX

$$$-a = a \iff a = 0$$$

Lean4

@[simp]
theorem neg_eq_self_iff {a : SignType} : -a = a ↔ a = 0 := by decide +revert

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

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

Разделы

Аффилиация

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