Theorems · Theorem · group theory

IsLocalHom.map_nonunit

∀ {R : Type u_2} {S : Type u_3} {F : Type u_5} {inst : Monoid R} {inst_1 : Monoid S} {inst_2 : FunLike F R S} {f : F}
  [self : IsLocalHom f] (a : R), IsUnit (f a) → IsUnit a

A local homomorphism f : R ⟶ S will send nonunits of R to nonunits of S.

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

8 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

IsLocalHom