zero_equiv_neg_iff

Mathlib.SetTheory.PGame.Algebra

URI: https://scilib.ai/kg/mathlib#SetTheory.PGame.zero_equiv_neg_iff

English

For all x: 0 ≈ -x iff 0 ≈ x.

Русский

Для любых x: 0 ≈ -x тогда и только тогда, когда 0 ≈ x.

LaTeX

$$$0 \approx -x \\iff 0 \approx x$$$

Lean4

@[simp]
theorem zero_equiv_neg_iff {x : PGame} : (0 ≈ -x) ↔ (0 ≈ x) := by rw [← neg_equiv_iff, neg_zero]

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

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

Разделы

Аффилиация

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