internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.subst_X
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
s : σ
⊢ subst a (X s) = a s
Tactic:
rw [← coe_substAlgHom ha, substAlgHom_X]
Proof state after:
no goals
Theorem: MvPowerSeries.subst_monomial
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
e : σ →₀ ℕ
r : R
⊢ subst a ((monomial R e) r) = (algebraMap R (MvPowerSeries τ S)) r * e.prod fun s n => a s ^ n
Tactic:
rw [← coe_substAlgHom ha, substAlgHom_monomial]
Proof state after:
no goals
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
letI : UniformSpace S := ⊥
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this : UniformSpace S := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this : UniformSpace S := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
letI : UniformSpace R := ⊥
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝ : UniformSpace S := ⊥
this : UniformSpace R := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝ : UniformSpace S := ⊥
this : UniformSpace R := ⊥
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
have := ((hasSum_aeval ha.evalDomain f).map (coeff S e) (continuous_coeff e))
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (coeff S e) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
erw [← this.tsum_eq, tsum_def]
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (if h : Summable fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b then
      if (Function.support fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b).Finite then
        ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b
      else Exists.choose h
    else 0) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ (if h : Summable fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b then
      if (Function.support fun b => (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b).Finite then
        ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b
      else Exists.choose h
    else 0) =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
erw [dif_pos this.summable, if_pos (coeff_subst_finite ha f e)]
Proof state after:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Theorem: MvPowerSeries.coeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : τ →₀ ℕ
this✝¹ : UniformSpace S := ⊥
this✝ : UniformSpace R := ⊥
this : HasSum (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((coeff S e) ((aeval ⋯) f))
⊢ ∑ᶠ (b : σ →₀ ℕ), (⇑(coeff S e) ∘ fun d => (coeff R d) f • d.prod fun s e => a s ^ e) b =
    ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (coeff S e) (d.prod fun s e => a s ^ e)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPowerSeries.constantCoeff_subst
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
⊢ (constantCoeff τ S) (subst a f) = ∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e)
Tactic:
simp only [← coeff_zero_eq_constantCoeff_apply, coeff_subst ha f 0]
Proof state after:
no goals
Theorem: MvPowerSeries.map_algebraMap_eq_subst_X
Proof state before:
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
⊢ (map σ (algebraMap R S)) f = subst X f
Tactic:
ext e
Proof state after:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (coeff S e) ((map σ (algebraMap R S)) f) = (coeff S e) (subst X f)
Theorem: MvPowerSeries.map_algebraMap_eq_subst_X
Proof state before:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (coeff S e) ((map σ (algebraMap R S)) f) = (coeff S e) (subst X f)
Tactic:
rw [coeff_map, coeff_subst substDomain_X f e, finsum_eq_single _ e]
Proof state after:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff R e) f) = (coeff R e) f • (coeff S e) (e.prod fun s e => X s ^ e)

case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff R x) f • (coeff S e) (x.prod fun s e => X s ^ e) = 0
Theorem: MvPowerSeries.map_algebraMap_eq_subst_X
Proof state before:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ (algebraMap R S) ((coeff R e) f) = (coeff R e) f • (coeff S e) (e.prod fun s e => X s ^ e)
Tactic:
rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_same,
  algebra_compatible_smul S, smul_eq_mul, mul_one]
Proof state after:
no goals
Theorem: MvPowerSeries.map_algebraMap_eq_subst_X
Proof state before:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e : σ →₀ ℕ
⊢ ∀ (x : σ →₀ ℕ), x ≠ e → (coeff R x) f • (coeff S e) (x.prod fun s e => X s ^ e) = 0
Tactic:
intro d hd
Proof state after:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e d : σ →₀ ℕ
hd : d ≠ e
⊢ (coeff R d) f • (coeff S e) (d.prod fun s e => X s ^ e) = 0
Theorem: MvPowerSeries.map_algebraMap_eq_subst_X
Proof state before:
case h
σ : Type u_1
inst✝⁸ : DecidableEq σ
A : Type u_2
inst✝⁷ : CommSemiring A
R : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : Algebra A R
τ : Type u_4
inst✝⁴ : DecidableEq τ
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra A S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
f : MvPowerSeries σ R
e d : σ →₀ ℕ
hd : d ≠ e
⊢ (coeff R d) f • (coeff S e) (d.prod fun s e => X s ^ e) = 0
Tactic:
rw [← MvPowerSeries.monomial_one_eq, coeff_monomial_ne hd.symm, smul_zero]
Proof state after:
no goals
Theorem: MvPowerSeries.comp_subst
Proof state before:
σ : Type u_1
inst✝¹⁸ : DecidableEq σ
A : Type u_2
inst✝¹⁷ : CommSemiring A
R : Type u_3
inst✝¹⁶ : CommRing R
inst✝¹⁵ : Algebra A R
τ : Type u_4
inst✝¹⁴ : DecidableEq τ
S : Type u_5
inst✝¹³ : CommRing S
inst✝¹² : Algebra A S
inst✝¹¹ : Algebra R S
inst✝¹⁰ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T : Type u_6
inst✝⁹ : CommRing T
inst✝⁸ : UniformSpace T
inst✝⁷ : T2Space T
inst✝⁶ : CompleteSpace T
inst✝⁵ : UniformAddGroup T
inst✝⁴ : TopologicalRing T
inst✝³ : LinearTopology T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ε : MvPowerSeries τ S →ₐ[R] T
this✝ : UniformSpace R := ⊥
this : UniformSpace S := ⊥
hε : Continuous ⇑ε
⊢ ⇑ε ∘ subst a = ⇑(aeval ⋯)
Tactic:
rw [← comp_substAlgHom ha hε, AlgHom.coe_comp, coe_substAlgHom]
Proof state after:
no goals
Theorem: MvPowerSeries.IsNilpotent_subst
Proof state before:
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ IsNilpotent ((constantCoeff τ S) ((substAlgHom ha) f))
Tactic:
rw [coe_substAlgHom, constantCoeff_subst ha]
Proof state after:
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ IsNilpotent (∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))
Theorem: MvPowerSeries.IsNilpotent_subst
Proof state before:
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ IsNilpotent (∑ᶠ (d : σ →₀ ℕ), (coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))
Tactic:
apply IsNilpotent.finsum
Proof state after:
case hf
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ ∀ (b : σ →₀ ℕ), IsNilpotent ((coeff R b) f • (constantCoeff τ S) (b.prod fun s e => a s ^ e))
Theorem: MvPowerSeries.IsNilpotent_subst
Proof state before:
case hf
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
⊢ ∀ (b : σ →₀ ℕ), IsNilpotent ((coeff R b) f • (constantCoeff τ S) (b.prod fun s e => a s ^ e))
Tactic:
intro d
Proof state after:
case hf
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
d : σ →₀ ℕ
⊢ IsNilpotent ((coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))
Theorem: MvPowerSeries.IsNilpotent_subst
Proof state before:
case hf
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
d : σ →₀ ℕ
⊢ IsNilpotent ((coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))
Tactic:
by_cases hd : d = 0
Proof state after:
case pos
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
d : σ →₀ ℕ
hd : d = 0
⊢ IsNilpotent ((coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))

case neg
σ : Type u_1
inst✝²³ : DecidableEq σ
A : Type u_2
inst✝²² : CommSemiring A
R : Type u_3
inst✝²¹ : CommRing R
inst✝²⁰ : Algebra A R
τ : Type u_4
inst✝¹⁹ : DecidableEq τ
S : Type u_5
inst✝¹⁸ : CommRing S
inst✝¹⁷ : Algebra A S
inst✝¹⁶ : Algebra R S
inst✝¹⁵ : IsScalarTower A R S
a : σ → MvPowerSeries τ S
ha : SubstDomain a
T✝ : Type u_6
inst✝¹⁴ : CommRing T✝
inst✝¹³ : UniformSpace T✝
inst✝¹² : T2Space T✝
inst✝¹¹ : CompleteSpace T✝
inst✝¹⁰ : UniformAddGroup T✝
inst✝⁹ : TopologicalRing T✝
inst✝⁸ : LinearTopology T✝
inst✝⁷ : Algebra R T✝
inst✝⁶ : Algebra S T✝
inst✝⁵ : IsScalarTower R S T✝
ε : MvPowerSeries τ S →ₐ[R] T✝
υ : Type u_7
inst✝⁴ : DecidableEq υ
T : Type u_8
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
b : τ → MvPowerSeries υ T
hb : SubstDomain b
f : MvPowerSeries σ R
hf : IsNilpotent ((constantCoeff σ R) f)
d : σ →₀ ℕ
hd : ¬d = 0
⊢ IsNilpotent ((coeff R d) f • (constantCoeff τ S) (d.prod fun s e => a s ^ e))