K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
⊢ a ^ q = a
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
⊢ a ^ q = a
have hp : 0 < Fintype.card K := lt_trans zero_lt_one Fintype.one_lt_card
case pos
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ a ^ q = a

case neg
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : ¬a = 0
⊢ a ^ q = a
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
⊢ a ^ q = a
by_cases h : a = 0
no goals
case neg
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : ¬a = 0
⊢ a ^ q = a
rw [← Nat.succ_pred_eq_of_pos hp, pow_succ, Nat.pred_eq_sub_one, pow_card_sub_one_eq_one a h,
  mul_one]
case pos
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ 0 ^ q = 0
case pos
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ a ^ q = a
rw [h]
no goals
case pos
K : Type u_1
R : Type ?u.294151
inst✝¹ : GroupWithZero K
inst✝ : Fintype K
a : K
hp : 0 < q
h : a = 0
⊢ 0 ^ q = 0
apply zero_pow hp