abelianizationCongr_trans — Mathlib

English

The induced abelianization map respects composition: the abelianization of a composition equals the composition of abelianizations.

Русский

Индуцированная абелизация сохраняет композицию: абелизация композиции равна композиции абелизаций.

LaTeX

$$$ (e \circ e')^{ab} = e^{ab} \circ (e')^{ab}. $$$

Lean4

@[simp]
theorem abelianizationCongr_trans {I : Type v} [Group I] (e : G ≃* H) (e₂ : H ≃* I) :
    e.abelianizationCongr.trans e₂.abelianizationCongr = (e.trans e₂).abelianizationCongr :=
  MulEquiv.toMonoidHom_injective (Abelianization.hom_ext _ _ rfl)

Похожие утверждения