bot_lt_toWithBotNat_iff — Mathlib

English

In a discrete valuation ring, the bottom is strictly less than the valuation of any nonzero element, i.e., ⊥ < toWithBotNat x iff x ≠ 0.

Русский

В дискретном оценочном кольце нуль меньше любой ненулевой величины; то есть ⊥ < toWithBotNat x эквивалентно x ≠ 0.

LaTeX

$$$\\bot < toWithBotNat(x) \\iff x \\neq 0$$$

Lean4

@[simp]
theorem bot_lt_toWithBotNat_iff (x : R) : ⊥ < toWithBotNat x ↔ x ≠ 0 := by rw [bot_lt_iff_ne_bot]; simp

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