neg_mem

Mathlib.RingTheory.Valuation.ValuationSubring

URI: https://scilib.ai/kg/mathlib#ValuationSubring.neg_mem

English

If x belongs to a valuation subring A, then −x also belongs to A.

Русский

Если x принадлежит валюационному подкольцу A, то и −x принадлежит A.

LaTeX

$$$\forall x\in K,\ x\in A \Rightarrow -x\in A$$$

Lean4

theorem neg_mem (x : K) : x ∈ A → -x ∈ A :=
  A.toSubring.neg_mem

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

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

Разделы

Аффилиация

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