Theorems · Theorem · commutative algebra

Function.Injective.isDomain

∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [IsDomain α] [inst_2 : Semiring β] {F : Type u_3}
  [inst_3 : FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F), Function.Injective ⇑f → IsDomain β

Pullback IsDomain instance along an injective function.

Defined in

Mathlib.Algebra.Ring.Hom.InjSurj

Cited by

27 results in Mathlib

Foundations

Depth 13 from the axioms · uses no axioms

Assumes

SemiringIsDomainSemiringFunLikeMonoidWithZeroHomClass