Theorem: PolynomialMap.ground_image_eq_coeff_sum_two (DividedPowers/PolynomialMap/Coeff.lean)

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ f.ground (r₁ • m₁ + r₂ • m₂) =
    ((coeff ![m₁, m₂]) f).sum fun k n => (∏ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i ^ k i) • n
Tactic:
suffices r₁ • m₁ + r₂ • m₂ = univ.sum fun i ↦ (![r₁, r₂]) i • (![m₁, m₂]) i  by
  rw [this, ground_image_eq_coeff_sum]
State after:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
⊢ r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i
Tactic:
simp
State after:
no goals

State before:
R : Type u
inst✝⁶ : CommRing R
M : Type uM
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type uN
inst✝³ : AddCommGroup N
inst✝² : Module R N
ι : Type uι
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
r₁ r₂ : R
m₁ m₂ : M
f : M →ₚ[R] N
this : r₁ • m₁ + r₂ • m₂ = ∑ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i • ![m₁, m₂] i
⊢ f.ground (r₁ • m₁ + r₂ • m₂) =
    ((coeff ![m₁, m₂]) f).sum fun k n => (∏ i : Fin (Nat.succ 0).succ, ![r₁, r₂] i ^ k i) • n
Tactic:
rw [this, ground_image_eq_coeff_sum]
State after:
no goals