case zero
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
⊢ a ⊗ₜ[R] b ^ Nat.zero = (a ^ Nat.zero) ⊗ₜ[R] (b ^ Nat.zero)

case succ
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
ih : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ a ⊗ₜ[R] b ^ Nat.succ k = (a ^ Nat.succ k) ⊗ₜ[R] (b ^ Nat.succ k)
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
⊢ a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
induction' k with k ih
no goals
case zero
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
⊢ a ⊗ₜ[R] b ^ Nat.zero = (a ^ Nat.zero) ⊗ₜ[R] (b ^ Nat.zero)
simp [one_def]
no goals
case succ
R : Type u
inst✝⁴ : CommSemiring R
A : Type v₁
inst✝³ : Semiring A
inst✝² : Algebra R A
B : Type v₂
inst✝¹ : Semiring B
inst✝ : Algebra R B
a : A
b : B
k : ℕ
ih : a ⊗ₜ[R] b ^ k = (a ^ k) ⊗ₜ[R] (b ^ k)
⊢ a ⊗ₜ[R] b ^ Nat.succ k = (a ^ Nat.succ k) ⊗ₜ[R] (b ^ Nat.succ k)
simp [pow_succ, ih]