intValuation_zero_lt — Mathlib

English

The valuation of a nonzero divisor is strictly positive: 0 < v.intValuation x for x ∈ nonZeroDivisors.

Русский

Оценка ненулевых делителей строго положительна: 0 < v.intValuation x для x ∈ nonZeroDivisors.

LaTeX

$$0 < v.intValuation(x) \quad (x \in \text{nonZeroDivisors})$$

Lean4

/-- Nonzero divisors have valuation greater than zero. -/
theorem intValuation_zero_lt (x : nonZeroDivisors R) : 0 < v.intValuation x :=
  by
  rw [v.intValuation_if_neg (nonZeroDivisors.coe_ne_zero x)]
  exact WithZero.zero_lt_coe _

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