self_eq_neg_iff

Mathlib.Data.Sign.Defs

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

English

An element a is equal to its negation if and only if a = 0.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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