English
There is a holding principle for liftOn' that if f satisfies f p 0 = f 0 1 for all p, then under a certain well-behavedness condition H, the lifted function satisfies f(p,q) equals the lifted value applied to p and q.
Русский
Существуют условия для liftOn', что если f(p,0)=f(0,1) для всех p и выполняются условия H, то f(p,q) равно значению liftOn' с p и q.
LaTeX
$$$ (\text{RatFunc.liftOn'} (p,q))\; f\; H = f(p,q) $$$
Lean4
@[simp]
theorem liftOn'_div {P : Sort v} (p q : K[X]) (f : K[X] → K[X] → P) (f0 : ∀ p, f p 0 = f 0 1) (H) :
(RatFunc.liftOn' (algebraMap _ (RatFunc K) p / algebraMap _ _ q)) f @H = f p q :=
by
rw [RatFunc.liftOn', liftOn_div _ _ _ f0]
apply liftOn_condition_of_liftOn'_condition H
