toWithBotNat_eq_bot_iff — Mathlib

English

Let R be a discrete valuation ring. For every x in R, the value of x under the discrete valuation is the bottom element if and only if x = 0.

Русский

Пусть R — локальное кольцо с дискретной оценкой. Для любого x ∈ R значение x в дискретной оценке равно нижнему элементу тогда и только тогда, когда x = 0.

LaTeX

$$$toWithBotNat(x) = \\bot \\iff x = 0$$$

Lean4

@[simp]
theorem toWithBotNat_eq_bot_iff (x : R) : toWithBotNat x = ⊥ ↔ x = 0 :=
  addVal_eq_top_iff

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