p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints { x // x ∈ H } (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints { x // x ∈ H } (Sylow p G) ↔ H ≤ normalizer ↑P
simp_rw [SetLike.le_def, ← Sylow.smul_eq_iff_mem_normalizer]
no goals
p : ℕ
G : Type u_1
inst✝ : Group G
H : Subgroup G
P : Sylow p G
⊢ P ∈ fixedPoints { x // x ∈ H } (Sylow p G) ↔ ∀ ⦃x : G⦄, x ∈ H → x • P = P
exact Subtype.forall