Theorems · Theorem · group theory

map_mul_eq_one

∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [MonoidHomClass F M N] (f : F) {a b : M}, a * b = 1 → f a * f b = 1

Defined in

Mathlib.Algebra.Group.Hom.Defs

Cited by

6 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

MulOneMulOneFunLikeMonoidHomClass