of_isDiscreteValuationRing

Mathlib.RingTheory.DiscreteValuationRing.Basic

URI: https://scilib.ai/kg/mathlib#of_isDiscreteValuationRing

English

Every discrete valuation ring is a valuation ring.

Русский

Каждое дискретное оценочное кольцо является оценочным кольцом.

LaTeX

$$$\\text{DVR}(R) \\Rightarrow \\text{ValuationRing}(R)$$$

Lean4

/-- A DVR is a valuation ring. -/
instance (priority := 100) of_isDiscreteValuationRing : ValuationRing A :=
  inferInstance

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

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

Разделы

Аффилиация

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