Theorems · Definition · field theory

RatFunc.liftMonoidWithZeroHom

{G₀ : Type u_1} →
  {R : Type u_3} →
    [inst : CommGroupWithZero G₀] →
      [inst_1 : CommRing R] →
        (φ : Polynomial R →*₀ G₀) →
          nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors G₀) → RatFunc R →*₀ G₀

Lift a monoid with zero homomorphism R[X] →*₀ G₀ to a R⟮X⟯ →*₀ G₀ on the condition that φ maps non-zero-divisors to non-zero-divisors, by mapping both the numerator and denominator and quotienting them.

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

CommGroupWithZeroCommRing