mem_ofSubring

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

x ∈ ofSubring(R,hR) iff x ∈ R.

Русский

x ∈ ofSubring(R,hR) тогда и только тогда, когда x ∈ R.

LaTeX

$$$x\in ofSubring(R,hR) \iff x\in R$$$

Lean4

@[simp]
theorem mem_ofSubring (R : Subring K) (hR : ∀ x : K, x ∈ R ∨ x⁻¹ ∈ R) (x : K) : x ∈ ofSubring R hR ↔ x ∈ R :=
  Iff.refl _

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

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

Разделы

Аффилиация

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