English
If the denominator evaluates to zero under f and a, then eval f a x equals zero.
Русский
Если знаменатель x при подстановке через f и a даёт ноль, то eval f a x равно нулю.
LaTeX
$$$ \text{Polynomial.eval}_2 f a (\operatorname{denom} x) = 0 \Rightarrow \mathrm{eval} f a x = 0$$$
Lean4
/-- Evaluate a rational function `p` given a ring hom `f` from the scalar field
to the target and a value `x` for the variable in the target.
Fractions are reduced by clearing common denominators before evaluating:
`eval id 1 ((X^2 - 1) / (X - 1)) = eval id 1 (X + 1) = 2`, not `0 / 0 = 0`.
-/
def eval (f : K →+* L) (a : L) (p : RatFunc K) : L :=
(num p).eval₂ f a / (denom p).eval₂ f a
