Theorem: DividedPowerAlgebra.isExponential_exp' (DividedPowers/DPAlgebra/Exponential.lean)

State before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (exp' R m).IsExponential
Tactic:
rw [isExponential_iff]
State after:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
        (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)

State before:
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1 ∧
    ∀ (p q : ℕ),
      ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
        (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
constructor
State after:
case left
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1

case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
      (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)

State before:
case left
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ (constantCoeff (DividedPowerAlgebra R M)) (exp' R m) = 1
Tactic:
rw [← coeff_zero_eq_constantCoeff, coeff_exp', dp_zero]
State after:
no goals

State before:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
⊢ ∀ (p q : ℕ),
    ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
      (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
intro p q
State after:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
    (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)

State before:
case right
R : Type u_1
inst✝⁶ : CommRing R
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
m : M
p q : ℕ
⊢ ↑((p + q).choose p) * (coeff (DividedPowerAlgebra R M) (p + q)) (exp' R m) =
    (coeff (DividedPowerAlgebra R M) p) (exp' R m) * (coeff (DividedPowerAlgebra R M) q) (exp' R m)
Tactic:
simp only [coeff_exp', dp_mul, nsmul_eq_mul]
State after:
no goals