Theorem: isCommutative_of_prime_order (Jordan/IndexNormal.lean)

State before:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
haveI := isCyclic_of_prime_card h
State after:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
this : IsCyclic G
⊢ Std.Commutative fun x x_1 => x * x_1

State before:
α : Type ?u.14086
inst✝³ : Fintype α
inst✝² : DecidableEq α
G : Type u_1
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
h : Fintype.card G = p
this : IsCyclic G
⊢ Std.Commutative fun x x_1 => x * x_1
Tactic:
exact Std.Commutative.mk (IsCyclic.commGroup.mul_comm)
State after:
no goals