mem_toSubring

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

Membership in the subring coincides with membership in the corresponding substructure.

Русский

Членство в подкольце совпадает с членством в соответствующей подструктуре.

LaTeX

$$$x \in A.toSubring \iff x \in A$$$

Lean4

@[simp]
theorem mem_toSubring (x : K) : x ∈ A.toSubring ↔ x ∈ A :=
  Iff.refl _

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

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

Разделы

Аффилиация

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