English
There exists a non-dependent recursion principle for RatFunc K: to construct a value for x, it suffices to specify a function on pairs p,q with a compatibility condition whenever q,q' are non-zero divisors.
Русский
Существует некоторые принципы рекурсии для RatFunc K: чтобы построить элемент, достаточно определить функцию на пары p,q с корректностью при q,q' ненулевых делителей.
LaTeX
$$$\\text{liftOn} : \\text{RatFunc}(K) \\to (\\text{Polynomial}K \\to \\text{Polynomial}K \\to P)$ with a compatibility condition$$
Lean4
/-- Non-dependent recursion principle for `RatFunc K`:
To construct a term of `P : Sort*` out of `x : RatFunc K`,
it suffices to provide a constructor `f : Π (p q : K[X]), P`
and a proof that `f p q = f p' q'` for all `p q p' q'` such that `q' * p = q * p'` where
both `q` and `q'` are not zero divisors, stated as `q ∉ K[X]⁰`, `q' ∉ K[X]⁰`.
If considering `K` as an integral domain, this is the same as saying that
we construct a value of `P` for such elements of `RatFunc K` by setting
`liftOn (p / q) f _ = f p q`.
When `[IsDomain K]`, one can use `RatFunc.liftOn'`, which has the stronger requirement
of `∀ {p q a : K[X]} (hq : q ≠ 0) (ha : a ≠ 0), f (a * p) (a * q) = f p q)`.
-/
def liftOn :=
val_proj @wrapped✝.{}
