Documentation

ClassificationOfSubgroups.Ch5_PropertiesOfSLOverAlgClosedField.S4_PropertiesOfCentralizers

Equations
  • =
Instances For
    theorem Field.self_eq_inv_iff {F : Type u} [Field F] (x : F) (x_ne_zero : x 0) :
    x = x⁻¹ x = 1 x = -1
    theorem Units.val_neg_one {F : Type u} [Field F] :
    (-1) = -1
    theorem Units.val_eq_neg_one {F : Type u} [Field F] (x : Fˣ) :
    x = -1 x = -1
    theorem centralizer_d_eq_D {F : Type u} [Field F] (δ : Fˣ) (δ_ne_one : δ 1) (δ_ne_neg_one : δ -1) :
    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) :
    theorem MulAut.conj_smul_symm {G : Type u_1} [Group G] (H K : Subgroup G) (c : G) (h : conj c H = K) :
    ∃ (c' : G), conj c' K = H