Theorems · Definition · field theory

RatFunc.liftRingHom

{L : Type u_2} →
  {R : Type u_3} →
    [inst : Field L] →
      [inst_1 : CommRing R] →
        (φ : Polynomial R →+* L) →
          nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L) → RatFunc R →+* L

Lift an injective ring homomorphism R[X] →+* L to a R⟮X⟯ →+* L by mapping both the numerator and denominator and quotienting them.

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

11 results in Mathlib

Foundations

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

Assumes

FieldCommRing