P3_neg

Mathlib.SetTheory.Surreal.Multiplication

URI: https://scilib.ai/kg/mathlib#Surreal.Multiplication.P3_neg

English

P3(x1, x2, y1, y2) holds iff P3(-x2, -x1, y1, y2) holds.

Русский

P3(x1, x2, y1, y2) эквивалентно P3(-x2, -x1, y1, y2).

LaTeX

$$$$ \mathrm{P3}(x_1,x_2,y_1,y_2) \iff \mathrm{P3}(-x_2,-x_1,y_1,y_2). $$$$

Lean4

theorem P3_neg : P3 x₁ x₂ y₁ y₂ ↔ P3 (-x₂) (-x₁) y₁ y₂ :=
  by
  simp_rw [P3, quot_neg_mul]
  rw [← _root_.neg_lt_neg_iff]
  abel_nf

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

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

Разделы

Аффилиация

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