instInhabited

Mathlib.RingTheory.Valuation.ValuationSubring

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

English

Same as mem_toSubring, but stated as a simp lemma.

Русский

То же с формулировкой упрощения слоем simp.

LaTeX

$$@[simp] theorem mem_toSubring (x : K) : x \in A.toSubring \iff x \in A$$

Lean4

instance : Inhabited (ValuationSubring K) :=
  ⟨⊤⟩

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

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

Разделы

Аффилиация

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