Documentation

Mathlib.Algebra.Hom.Ring.Basic

Additional lemmas about homomorphisms of semirings and rings #

These lemmas have been banished here to avoid unnecessary imports in Mathlib.Algebra.Hom.Ring.Defs.

They could be moved to more natural homes.

theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero {α : Type u_2} {β : Type u_3} :
∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), 0 = 1 Set.range f = {0}

f : α →+* β has a trivial codomain iff its range is {0}.

theorem RingHom.isUnit_map {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] (f : α →+* β) {a : α} :
IsUnit aIsUnit (f a)
theorem RingHom.map_dvd {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] (f : α →+* β) {a : α} {b : α} :
a bf a f b
theorem Function.Injective.isDomain {α : Type u_2} {β : Type u_3} [Ring α] [IsDomain α] [Ring β] (f : β →+* α) (hf : Function.Injective f) :

Pullback IsDomain instance along an injective function.