neg_mem

Mathlib.FieldTheory.IntermediateField.Basic

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

English

If x belongs to an intermediate field S, then its additive inverse −x also belongs to S.

Русский

Если x ∈ S, то −x ∈ S.

LaTeX

$$$\forall x \in L,\ x \in S \Rightarrow -x \in S$$$

Lean4

protected theorem neg_mem {x : L} (hx : x ∈ S) : -x ∈ S := by change -x ∈ S.toSubalgebra; simpa

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

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

Разделы

Аффилиация

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