Theorems · Theorem · field theory

RatFunc.map_injective

∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))),
  Function.Injective ⇑φ → Function.Injective ⇑(RatFunc.map φ hφ)

Defined in

Mathlib.FieldTheory.RatFunc.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingFunLikeMonoidHomClass