Theorems · Definition · field theory

RatFunc.liftOn

{K : Type u_1} →
  [inst : CommRing K] →
    {P : Sort u_2} →
      RatFunc K →
        (f : Polynomial K → Polynomial K → P) →
          (∀ {p q p' q' : Polynomial K},
              q ∈ nonZeroDivisors (Polynomial K) →
                q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q') →
            P

Non-dependent recursion principle for K⟮X⟯: To construct a term of P : Sort* out of x : K⟮X⟯, 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 K⟮X⟯ 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).

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

6 results in Mathlib

Foundations

Depth 98 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing