Theorem: alternatingGroup.V4_isCommutative (Jordan/V4.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα4 : Fintype.card α = 4
⊢ Subgroup.IsCommutative (V4 α)
Tactic:
refine' { is_comm := isCommutative_of_exponent_two (V4_is_of_exponent_two α hα4) }
State after:
no goals