conjMap_comp — Mathlib

English

If k = h g, then the conjugation maps compose according to the product: conjMap hh after conjMap hg equals conjMap hk.

Русский

Если k = h g, то конъюгирующие отображения удовлетворяют правилу композиции: conjMap hh ∘ conjMap hg = conjMap hk.

LaTeX

$$$\\text{If } k = h g,\\; (\\text{conjMap}_{hh}) \\circ (\\text{conjMap}_{hg}) = \\text{conjMap}_{hk}.$$$

Lean4

@[to_additive]
theorem conjMap_comp (H : k = h * g) :
    (conjMap hh).comp (conjMap hg) (κ := stabilizerEquivStabilizer_compTriple H) = conjMap hk :=
  by
  ext x
  simpa using conjMap_comp_apply H x

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