eq_zero_of_mem_of_neg_mem

Mathlib.Algebra.Order.Ring.Ordering.Basic

URI: https://scilib.ai/kg/mathlib#RingPreordering.eq_zero_of_mem_of_neg_mem

← MathLib Explorer

English

If x ∈ F and -x ∈ F for a field F, then x = 0.

Русский

Пусть x ∈ F и -x ∈ F для поля F, тогда x = 0.

LaTeX

$$$\forall x\, x \in P \land -x \in P \Rightarrow x = 0$$$

Lean4

@[aesop unsafe 70% apply]
protected theorem eq_zero_of_mem_of_neg_mem {x} (h : x ∈ P) (h2 : -x ∈ P) : x = 0 :=
  by
  by_contra
  have mem : -x * x⁻¹ ∈ P := by aesop (erase simp neg_mul)
  field_simp at mem
  exact RingPreordering.neg_one_notMem P mem

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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