Theorems · Theorem · group theory

MulEquiv.toAdditive_symm_apply_symm_apply

∀ {G : Type u_2} {H : Type u_3} [inst : MulOneClass G] [inst_1 : MulOneClass H] (f : Additive G ≃+ Additive H) (a : H),
  (MulEquiv.toAdditive.symm f).symm a = (MonoidHom.toAdditive.symm f.symm.toAddMonoidHom) a

Defined in

Mathlib.Algebra.Group.Equiv.TypeTags

Cited by

0 results in Mathlib

Foundations

Depth 22 from the axioms · uses Quot.sound

Assumes

MulOneClassMulOneClass