addVal_zero

Mathlib.RingTheory.DiscreteValuationRing.Basic

URI: https://scilib.ai/kg/mathlib#IsDiscreteValuationRing.addVal_zero

English

The additive valuation of zero is the top element of the valuation order.

Русский

Плюс-оценка нуля равна верхнему элементу упорядочения оценки.

LaTeX

$$$\mathrm{addVal}(0) = \top$$$

Lean4

theorem addVal_zero : addVal R 0 = ⊤ :=
  (addVal R).map_zero

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

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

Разделы

Аффилиация

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