English
There is an induction principle for RatFunc K: if a predicate holds for all representations p/q, then it holds for every element of RatFunc K.
Русский
Существуют принципы индукции для RatFunc K: если условие P выполняется для всех представлений p/q, тогда выполняется для каждого элемента RatFunc K.
LaTeX
$$Protected induction: For any P: RatFunc K → Prop, P(x) holds if P(p/q) holds for all p,q with q ≠ 0.$$
Lean4
/-- Induction principle for `RatFunc K`: if `f p q : P (p / q)` for all `p q : K[X]`,
then `P` holds on all elements of `RatFunc K`.
See also `induction_on'`, which is a recursion principle defined in terms of `RatFunc.mk`.
-/
protected theorem induction_on {P : RatFunc K → Prop} (x : RatFunc K)
(f : ∀ (p q : K[X]) (_ : q ≠ 0), P (algebraMap _ (RatFunc K) p / algebraMap _ _ q)) : P x :=
x.induction_on' fun p q hq => by simpa using f p q hq
