Theorems · Theorem · group theory

QuotientGroup.homQuotientZPowOfHom_comp_of_rightInverse

∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (f : A →* B) (g : B →* A) (n : ℤ),
  Function.RightInverse ⇑g ⇑f →
    (QuotientGroup.homQuotientZPowOfHom f n).comp (QuotientGroup.homQuotientZPowOfHom g n) =
      MonoidHom.id (B ⧸ (zpowGroupHom n).range)

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

Depth 80 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommGroupCommGroup