Theorem: MvPowerSeries.prod_smul_X_eq_smul_monomial_one (DividedPowers/ForMathlib/MvPowerSeries/Substitutions.lean)

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => (a s • X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1
Tactic:
rw [Finsupp.prod_congr (g2 := fun s n ↦ ((C σ R (algebraMap A R (a s)) * (X s : MvPowerSeries σ R)) ^ n))]
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => ((C σ R) ((algebraMap A R) (a s)) * X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (e.prod fun s n => ((C σ R) ((algebraMap A R) (a s)) * X s) ^ n) = (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
simp only [mul_pow, Finsupp.prod_mul]
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((e.prod fun a_1 b => (C σ R) ((algebraMap A R) (a a_1)) ^ b) * e.prod fun a b => X a ^ b) =
    (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((e.prod fun a_1 b => (C σ R) ((algebraMap A R) (a a_1)) ^ b) * e.prod fun a b => X a ^ b) =
    (e.prod fun s n => a s ^ n) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
simp only [← map_pow, ← map_finsupp_prod]
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * e.prod fun a b => X a ^ b) =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ((C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * e.prod fun a b => X a ^ b) =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [← monomial_one_eq]
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * (monomial R e) 1 =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ (C σ R) ((algebraMap A R) (e.prod fun a_1 b => a a_1 ^ b)) * (monomial R e) 1 =
    (e.prod fun a_1 b => a a_1 ^ b) • (monomial R e) 1

σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [← smul_eq_C_mul, ← algebra_compatible_smul]
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
⊢ ∀ x ∈ e.support, (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
intro x _
State after:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x

State before:
σ : Type u_1
A : Type u_2
inst✝² : CommSemiring A
R : Type u_3
inst✝¹ : CommSemiring R
inst✝ : Algebra A R
e : σ →₀ ℕ
a : σ → A
x : σ
a✝ : x ∈ e.support
⊢ (a x • X x) ^ e x = ((C σ R) ((algebraMap A R) (a x)) * X x) ^ e x
Tactic:
rw [algebra_compatible_smul R, smul_eq_C_mul]
State after:
no goals