Theorems · Theorem · field theory

RatFunc.liftRingHom_injective

∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] [Nontrivial R] (φ : Polynomial R →+* L)
  (hφ : Function.Injective ⇑φ)
  (hφ' : optParam (nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)) ⋯),
  Function.Injective ⇑(RatFunc.liftRingHom φ hφ')

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldCommRingNontrivial