theorem
centralizer_d_eq_D'
{F : Type u}
[Field F]
(δ : Fˣ)
(hd : SpecialMatrices.d δ ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F))
:
theorem
centralizer_neg_eq_centralizer
{F : Type u}
[Field F]
{x : Matrix.SpecialLinearGroup (Fin 2) F}
:
theorem
conjugate_centralizers_of_IsConj
{G : Type u}
[Group G]
(a b : G)
(hab : IsConj a b)
:
∃ (x : G), MulAut.conj x • Subgroup.centralizer {a} = Subgroup.centralizer {b}
theorem
conjugate_IsComm_of_IsComm'
{G : Type u_1}
[Group G]
(c : G)
(H K : Subgroup G)
(hK : K.IsCommutative)
(h : MulAut.conj c • K = H)
:
theorem
conjugate_IsComm_of_IsComm
{G : Type u_1}
[Group G]
(c : G)
(K : Subgroup G)
(hK : K.IsCommutative)
:
(MulAut.conj c • K).IsCommutative
theorem
IsCommutative_centralizer_of_not_mem_center
{F : Type u}
[Field F]
[IsAlgClosed F]
[DecidableEq F]
(x : Matrix.SpecialLinearGroup (Fin 2) F)
(hx : x ∉ Subgroup.center (Matrix.SpecialLinearGroup (Fin 2) F))
: