Theorems · Theorem · field theory

RatFunc.liftOn_ofFractionRing_mk

∀ {K : Type u} [inst : CommRing K] {P : Sort v} (n : Polynomial K) (d : ↥(nonZeroDivisors (Polynomial K)))
  (f : Polynomial K → Polynomial K → P)
  (H :
    ∀ {p q p' q' : Polynomial K},
      q ∈ nonZeroDivisors (Polynomial K) → q' ∈ nonZeroDivisors (Polynomial K) → q' * p = q * p' → f p q = f p' q'),
  { toFractionRing := Localization.mk n d }.liftOn f H = f n ↑d

Defined in

Mathlib.FieldTheory.RatFunc.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRing