conjMap_comp_inv_apply — Mathlib

English

Conjugation by an inverse maps back to the original element after applying conjugation twice.

Русский

Угол конъугации обратной приводит к исходному элементу после повторной конъугации.

LaTeX

$$$\text{conjMap\_inv\_apply}: (conjMap (eq\_inv\_smul\_iff.mpr hg.symm)) (conjMap hg x) = x$$$

Lean4

@[to_additive]
theorem conjMap_comp_inv_apply (x : ofStabilizer G a) : (conjMap (eq_inv_smul_iff.mpr hg.symm)) (conjMap hg x) = x := by
  simp [← Subtype.coe_inj, conjMap_apply]

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