Theorems · Theorem · group theory

isUnit_map_iff

∀ {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]
  [MonoidHomClass F R S] (f : F) [IsLocalHom f] (a : R), IsUnit (f a) ↔ IsUnit a

Defined in

Mathlib.Algebra.Group.Units.Hom

Cited by

17 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext

Assumes

MonoidMonoidFunLikeMonoidHomClassIsLocalHom