abelianizationCongr_refl — Mathlib

English

The abelianization congruence of the identity on G equals the identity on the abelianization of G.

Русский

Конгруэнтность абелизации для тождества на G совпадает с тождественным отображением на G^{ab}.

LaTeX

$$$ (\mathrm{Id}_G)^{ab} = \mathrm{Id}_{G^{ab}}. $$$

Lean4

@[simp]
theorem abelianizationCongr_refl : (MulEquiv.refl G).abelianizationCongr = MulEquiv.refl (Abelianization G) :=
  MulEquiv.toMonoidHom_injective Abelianization.lift_of

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