conj_mem_fixingSubgroup — Mathlib

English

Conjugation induces a bijection between fixingSubgroups of translates.

Русский

Конъюгация индуцирует биекция между фиксирующими подгруппами переносов.

LaTeX

$$$conjMap_ofFixingSubgroup\ (hst) : fixingSubgroup M t \to fixingSubgroup M s$ is bijective$$

Lean4

@[to_additive]
theorem _root_.Set.conj_mem_fixingSubgroup (hg : g • t = s) {k : M} (hk : k ∈ fixingSubgroup M t) :
    MulAut.conj g k ∈ fixingSubgroup M s :=
  by
  simp only [mem_fixingSubgroup_iff] at hk ⊢
  intro y hy
  rw [MulAut.conj_apply, eq_comm, mul_smul, mul_smul, ← inv_smul_eq_iff, eq_comm]
  apply hk
  rw [← Set.mem_smul_set_iff_inv_smul_mem, hg]
  exact hy

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