α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 (_root_.orderOf g)
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ IsThreeCycle (g * g)
rw [← pow_two, ← card_support_eq_three_iff, support_pow_coprime, ht.card_support]
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 3
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 (_root_.orderOf g)
rw [ht.orderOf]
no goals
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ g : Perm α
ht : IsThreeCycle g
⊢ Nat.coprime 2 3
norm_num