toWithBotNat_zero

Mathlib.RingTheory.DiscreteValuationRing.Basic

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

English

The valuation at zero corresponds to the bottom element under WithBot Nat.

Русский

Значение оценки нуля соответствует нижнему элементу WithBot Nat.

LaTeX

$$$\mathrm{toWithBotNat}(0) = \bot$$$

Lean4

@[simp]
theorem toWithBotNat_zero : toWithBotNat (R := R) 0 = ⊥ :=
  addVal_zero

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

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

Разделы

Аффилиация

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