toWithBotNat

Mathlib.RingTheory.DiscreteValuationRing.Basic

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

English

The new valuation function toWithBotNat is simply addVal; it maps elements to WithBot ℕ.

Русский

Новая функция оценки toWithBotNat есть просто addVal; она отображает элементы в WithBot ℕ.

LaTeX

$$$\mathrm{toWithBotNat} = \mathrm{addVal}$$$

Lean4

/-- A modification of the valuation, sending `0` to `⊥` instead of `⊤`. -/
def toWithBotNat (x : R) : WithBot ℕ :=
  addVal R x

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

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

Разделы

Аффилиация

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