English
For x,y with nonzero denominators, eval f a (x * y) = eval f a x * eval f a y.
Русский
При ненулевых знаменателях eval f a (x y) = eval f a x · eval f a y.
LaTeX
$$$ \mathrm{eval} f a (x \cdot y) = \mathrm{eval} f a x \cdot \mathrm{eval} f a y $$$
Lean4
/-- `eval` is an additive homomorphism except when a denominator evaluates to `0`.
Counterexample: `eval _ 1 (X / (X-1)) + eval _ 1 (-1 / (X-1)) = 0`
`... ≠ 1 = eval _ 1 ((X-1) / (X-1))`.
See also `RatFunc.eval₂_denom_ne_zero` to make the hypotheses simpler but less general.
-/
theorem eval_add {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_add_dvd x y) hxy
rw [Polynomial.eval₂_mul] at this
cases mul_eq_zero.mp this <;> contradiction
rw [div_add_div _ _ hx hy, eq_div_iff (mul_ne_zero hx hy), div_eq_mul_inv, mul_right_comm, ← div_eq_mul_inv,
div_eq_iff hxy]
simp only [← Polynomial.eval₂_mul, ← Polynomial.eval₂_add]
congr 1
apply num_denom_add
