Theorem: MetabelianGroup.kernel_pow (UnitConjecture/MetabelianGroup.lean)

State before:
Q : Type u_1
K : Type u_2
inst✝¹ : AddGroup Q
inst✝ : AddCommGroup K
c : Q → Q → K
ccl : Cocycle c
k : K
n : ℕ
⊢ (k, 0) ^ n = (n • k, 0)
Tactic:
induction n <;>
    aesop (rule_sets [Metabelian, Cocycle]) 
    (add norm simp [pow_zero, pow_succ, zero_nsmul, succ_nsmul])
State after:
no goals