G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ Characteristic ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
⊢ Characteristic ↑P
haveI := Sylow.subsingleton_of_normal P h
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ ∀ (ϕ : G ≃* G), Subgroup.map (MulEquiv.toMonoidHom ϕ) ↑P = ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ Characteristic ↑P
rw [characteristic_iff_map_eq]
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Subgroup.map (MulEquiv.toMonoidHom Φ) ↑P = ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
⊢ ∀ (ϕ : G ≃* G), Subgroup.map (MulEquiv.toMonoidHom ϕ) ↑P = ↑P
intro Φ
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ ↑(Φ • P) = ↑P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Subgroup.map (MulEquiv.toMonoidHom Φ) ↑P = ↑P
show (Φ • P).toSubgroup = P.toSubgroup
case e_self
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Φ • P = P
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ ↑(Φ • P) = ↑P
congr
no goals
case e_self
G : Type u
α : Type v
β : Type w
inst✝² : Group G
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
h : Normal ↑P
this : Subsingleton (Sylow p G)
Φ : G ≃* G
⊢ Φ • P = P
simp