English
The valuation of X with respect to the height-one spectrum idealX K equals exp(-1) in WithZero; i.e., valuation is -1.
Русский
Оценка X по отношению к идеалу высоты один равна exp(-1).
LaTeX
$$$ \operatorname{valuation}(\mathrm{idealX } K) (\mathrm{RatFunc } K) (\mathrm{X}) = \mathrm{WithZero}.exp(-1) $$$
Lean4
/-- This is the principal ideal generated by `X` in the ring of polynomials over a field K,
regarded as an element of the height-one-spectrum. -/
def idealX : IsDedekindDomain.HeightOneSpectrum K[X]
where
asIdeal := Ideal.span { X }
isPrime := by rw [Ideal.span_singleton_prime]; exacts [Polynomial.prime_X, Polynomial.X_ne_zero]
ne_bot := by rw [ne_eq, Ideal.span_singleton_eq_bot]; exact Polynomial.X_ne_zero
