abelianizationCongr_symm — Mathlib

English

The abelianization congruence is symmetric with respect to the inverse isomorphism: e^{ab} equals the abelianization of e^{-1}.

Русский

Конгруэнтность абелизации симметрична по отношению к обратному изоморфизму: e^{ab} = (e^{-1})^{ab}.

LaTeX

$$$ e^{ab\}{}^{ -1} = (e^{-1})^{ab}. $$$

Lean4

@[simp]
theorem abelianizationCongr_symm (e : G ≃* H) : e.abelianizationCongr.symm = e.symm.abelianizationCongr :=
  rfl

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