mem_or_inv_mem

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

For any x in K, either x is in the valuation subring or its inverse is.

Русский

Для любого x в K либо x принадлежит валюационному подкольцу, либо его обратное принадлежит подкольцу.

LaTeX

$$$\forall x\in K,\ x\in A \lor x^{-1} \in A$$$

Lean4

theorem mem_or_inv_mem (x : K) : x ∈ A ∨ x⁻¹ ∈ A :=
  A.mem_or_inv_mem' _

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

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

Разделы

Аффилиация

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