no goals
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
n : ℕ
x : α
⊢ Commute (↑n) x
induction n with
| zero => rw [Nat.cast_zero]; exact Commute.zero_left x
| succ n ihn => rw [Nat.cast_succ]; exact ihn.add_left (Commute.one_left x)
case zero
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
case zero
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
⊢ Commute (↑zero) x
rw [Nat.cast_zero]
no goals
case zero
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
⊢ Commute 0 x
exact Commute.zero_left x
case succ
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x
case succ
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑(succ n)) x
rw [Nat.cast_succ]
no goals
case succ
α : Type u_1
β : Type ?u.6256
inst✝ : NonAssocSemiring α
x : α
n : ℕ
ihn : Commute (↑n) x
⊢ Commute (↑n + 1) x
exact ihn.add_left (Commute.one_left x)