fixingSubgroupEquivFixingSubgroup

English

There exists a natural MulEquiv between fixingSubgroups for translate pairs.

Русский

Существует естественный MulEquiv между фиксирующими подгруппами для пары переносов.

LaTeX

$$$fixingSubgroupEquivFixingSubgroup (hg) : fixingSubgroup M t \cong fixingSubgroup M s$$$

Lean4

/-- The equivalence of `fixingSubgroup M t` with `fixingSubgroup M s`
  when `s` is a translate of `t`. -/
@[to_additive /-- The equivalence of `fixingSubgroup M t` with `fixingSubgroup M s`
      when `s` is a translate of `t`. -/
    ]
def fixingSubgroupEquivFixingSubgroup (hg : g • t = s) : fixingSubgroup M t ≃* fixingSubgroup M s :=
  ((MulAut.conj g).subgroupMap (fixingSubgroup M t)).trans (MulEquiv.subgroupCongr (fixingSubgroup_map_conj_eq hg))

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