Theorems · Theorem · field theory

RatFunc.liftOn_div

∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {P : Sort v} (p q : Polynomial K)
  (f : Polynomial K → Polynomial K → P),
  (∀ (p : Polynomial K), f p 0 = f 0 1) →
    ∀ (H' : ∀ {p q p' q' : Polynomial K}, q ≠ 0 → q' ≠ 0 → q' * p = q * p' → f p q = f p' q')
      (H :
        optParam
          (∀ {p q p' q' : Polynomial K},
            q ∈ nonZeroDivisors (Polynomial K) →
              q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q')
          ⋯),
      ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).liftOn f H = f p q

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingIsDomain