Theorem: PowerSeries.isExponential_iff (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⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧ ∀ (p q : ℕ), ↑((p + q).choose p) * (coeff R (p + q)) f = (coeff R p) f * (coeff R q) f
Tactic:
rw [← isExponential_add_mul_iff]
State after:
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⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f

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⟧
⊢ f.IsExponential ↔
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f
Tactic:
constructor
State after:
case mp
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⟧
⊢ f.IsExponential →
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f

case mpr
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⟧
⊢ (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f →
    f.IsExponential

State before:
case mp
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⟧
⊢ f.IsExponential →
    (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f
Tactic:
exact fun hf ↦ ⟨hf.constantCoeff, hf.add_mul⟩
State after:
no goals

State before:
case mpr
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⟧
⊢ (constantCoeff R) f = 1 ∧
      subst (MvPowerSeries.X 0 + MvPowerSeries.X 1) f = subst (MvPowerSeries.X 0) f * subst (MvPowerSeries.X 1) f →
    f.IsExponential
Tactic:
exact fun hf ↦ {
  constantCoeff := hf.1
  add_mul := hf.2 }
State after:
no goals