Theorem: PowerSeries.isExponential_npow (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
⊢ (f ^ n).IsExponential
Tactic:
induction n with
| zero =>
  simp only [Nat.zero_eq, pow_zero]
  exact isExponential_one
| succ n hn =>
  rw [pow_succ]
  exact isExponential_mul hn hf
State after:
no goals

State before:
case zero
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ (f ^ 0).IsExponential
Tactic:
simp only [Nat.zero_eq, pow_zero]
State after:
case zero
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ IsExponential 1

State before:
case zero
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
⊢ IsExponential 1
Tactic:
exact isExponential_one
State after:
no goals

State before:
case succ
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ (n + 1)).IsExponential
Tactic:
rw [pow_succ]
State after:
case succ
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ n * f).IsExponential

State before:
case succ
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
f : R⟦X⟧
hf : f.IsExponential
n : ℕ
hn : (f ^ n).IsExponential
⊢ (f ^ n * f).IsExponential
Tactic:
exact isExponential_mul hn hf
State after:
no goals