Theorems · Theorem · field theory

RatFunc.liftRingHom_ofFractionRing_algebraMap

∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] (φ : Polynomial R →+* L)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) (x : Polynomial R),
  (RatFunc.liftRingHom φ hφ) { toFractionRing := (algebraMap (Polynomial R) (FractionRing (Polynomial R))) x } = φ x

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldCommRing