case zero
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ ↑(χ ^ Nat.zero) ↑a = ↑χ ↑a ^ Nat.zero

case succ
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : ↑(χ ^ n) ↑a = ↑χ ↑a ^ n
⊢ ↑(χ ^ Nat.succ n) ↑a = ↑χ ↑a ^ Nat.succ n
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
a : Rˣ
⊢ ↑(χ ^ n) ↑a = ↑χ ↑a ^ n
induction' n with n ih
no goals
case zero
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
⊢ ↑(χ ^ Nat.zero) ↑a = ↑χ ↑a ^ Nat.zero
rw [pow_zero, pow_zero, one_apply_coe]
no goals
case succ
R : Type u
inst✝¹ : CommMonoid R
R' : Type v
inst✝ : CommMonoidWithZero R'
χ : MulChar R R'
a : Rˣ
n : ℕ
ih : ↑(χ ^ n) ↑a = ↑χ ↑a ^ n
⊢ ↑(χ ^ Nat.succ n) ↑a = ↑χ ↑a ^ Nat.succ n
rw [pow_succ, pow_succ, mul_apply, ih]