Theorems · Theorem · group theory

OneHom.mk.congr_simp

∀ {M : Type u_10} {N : Type u_11} [inst : One M] [inst_1 : One N] (toFun toFun_1 : M → N) (e_toFun : toFun = toFun_1)
  (map_one' : toFun 1 = 1), { toFun := toFun, map_one' := map_one' } = { toFun := toFun_1, map_one' := ⋯ }

Defined in

Mathlib.Algebra.Group.Equiv.TypeTags

Cited by

21 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms

Assumes

OneOne