domCongr_symm — Mathlib

English

The domCongr construction is symmetric with respect to inverses: domCongr k A e).symm = domCongr k A e.symm.

Русский

Конструкция domCongr симметрична к инверсии: domCongr k A e).symm = domCongr k A e.symm.

LaTeX

$$$\\mathrm{domCongr}\\ k\\;A\\;e)^{\\mathrm{symm}} = \\mathrm{domCongr}\\ k\\;A\\;e^{\\mathrm{symm}}$$$

Lean4

@[to_additive (attr := simp)]
theorem domCongr_symm (e : G ≃* H) : (domCongr k A e).symm = domCongr k A e.symm :=
  rfl

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