English
The ideal generated by X in the polynomial ring K[X] gives a height-one prime spectrum element in IsDedekindDomain.HeightOneSpectrum K[X].
Русский
Идеал, порождённый X в кольце многочленов K[X], образует элемент спектра высоты один в IsDedekindDomain.HeightOneSpectrum K[X].
LaTeX
$$$ \text{idealX } K \;:\; \mathrm{IsDedekindDomain.HeightOneSpectrum } K[X] $$$
Lean4
/-- `eval` is a multiplicative homomorphism except when a denominator evaluates to `0`.
Counterexample: `eval _ 0 X * eval _ 0 (1/X) = 0 ≠ 1 = eval _ 0 1 = eval _ 0 (X * 1/X)`.
See also `RatFunc.eval₂_denom_ne_zero` to make the hypotheses simpler but less general.
-/
theorem eval_mul {x y : RatFunc K} (hx : Polynomial.eval₂ f a (denom x) ≠ 0) (hy : Polynomial.eval₂ f a (denom y) ≠ 0) :
eval f a (x * y) = eval f a x * eval f a y := by
unfold eval
by_cases hxy : Polynomial.eval₂ f a (denom (x * y)) = 0
· have := Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero f a (denom_mul_dvd x y) hxy
rw [Polynomial.eval₂_mul] at this
cases mul_eq_zero.mp this <;> contradiction
rw [div_mul_div_comm, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ← div_eq_mul_inv,
div_eq_iff hxy]
repeat' rw [← Polynomial.eval₂_mul]
congr 1
apply num_denom_mul
