Generalities on the polynomial structure of rational functions #
Main definitions #
RatFunc.C
is the constant polynomialRatFunc.X
is the indeterminateRatFunc.eval
evaluates a rational function given a value for the indeterminate
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
.
Equations
- RatFunc.eval f a p = Polynomial.eval₂ f a p.num / Polynomial.eval₂ f a p.denom
Instances For
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.
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.