English
For any MonoidWithZero homomorphism φ, the lifted RatFunc evaluates as the quotient of the mapped numerator and denominator: liftMonoidWithZeroHom φ hφ f = φ(f.num) / φ(f.denom).
Русский
Для любого гомоморфизма MonoidWithZero φ выполняется, что возведенная в RatFunc функция равна отношению образов числителя и знаменателя: liftMonoidWithZeroHom φ hφ f = φ(f.num) / φ(f.denom).
LaTeX
$$$\\operatorname{liftMonoidWithZeroHom}(\\phi, h\\phi)(f) = \\dfrac{\\phi(f\\text{.num})}{\\phi(f\\text{.denom})}$$$
Lean4
theorem liftMonoidWithZeroHom_apply {L : Type*} [CommGroupWithZero L] (φ : K[X] →*₀ L) (hφ : K[X]⁰ ≤ L⁰.comap φ)
(f : RatFunc K) : liftMonoidWithZeroHom φ hφ f = φ f.num / φ f.denom := by
rw [← num_div_denom f, liftMonoidWithZeroHom_apply_div, num_div_denom]
