internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.hasSum_aeval
Proof state before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
have := hasSum_eval₂ (continuous_algebraMap R S) ha f
Proof state after:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (algebraMap R S) ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Theorem: MvPowerSeries.hasSum_aeval
Proof state before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (algebraMap R S) ((coeff R d) f) * d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
simp_rw [← smul_eq_mul, algebraMap_smul] at this
Proof state after:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Theorem: MvPowerSeries.hasSum_aeval
Proof state before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) ((aeval ha) f)
Tactic:
rw [coe_aeval]
Proof state after:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
Theorem: MvPowerSeries.hasSum_aeval
Proof state before:
σ : Type u_1
inst✝¹² : DecidableEq σ
R : Type u_2
inst✝¹¹ : CommRing R
inst✝¹⁰ : UniformSpace R
inst✝⁹ : UniformAddGroup R
inst✝⁸ : TopologicalRing R
S : Type u_3
inst✝⁷ : CommRing S
inst✝⁶ : UniformSpace S
inst✝⁵ : UniformAddGroup S
inst✝⁴ : TopologicalRing S
inst✝³ : T2Space S
inst✝² : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f✝ : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹ : Algebra R S
inst✝ : ContinuousSMul R S
f : MvPowerSeries σ R
this : HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
⊢ HasSum (fun d => (coeff R d) f • d.prod fun s e => a s ^ e) (eval₂ (algebraMap R S) a f)
Tactic:
exact this
Proof state after:
no goals
Theorem: MvPowerSeries.comp_aeval
Proof state before:
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (aeval ha) = aeval ⋯
Tactic:
apply DFunLike.coe_injective
Proof state after:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ (fun f => ⇑f) (ε.comp (aeval ha)) = (fun f => ⇑f) (aeval ⋯)
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ (fun f => ⇑f) (ε.comp (aeval ha)) = (fun f => ⇑f) (aeval ⋯)
Tactic:
simp only [AlgHom.coe_comp, coe_aeval ha]
Proof state after:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ (algebraMap R S) a = ⇑(aeval ⋯)
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ eval₂ (algebraMap R S) a = ⇑(aeval ⋯)
Tactic:
erw [comp_eval₂ (continuous_algebraMap R S) ha hε]
Proof state after:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ eval₂ (ε.comp (algebraMap R S)) (⇑ε.toRingHom ∘ a) = ⇑(aeval ⋯)
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ eval₂ (ε.comp (algebraMap R S)) (⇑ε.toRingHom ∘ a) = ⇑(aeval ⋯)
Tactic:
apply congr_arg₂
Proof state after:
case a.hx
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (algebraMap R S) = algebraMap R T

case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a.hx
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ε.comp (algebraMap R S) = algebraMap R T

case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Tactic:
simp only [AlgHom.toRingHom_eq_coe, AlgHom.comp_algebraMap_of_tower]
Proof state after:
case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε.toRingHom ∘ a = fun n => (fun s => ε.toRingHom (a s)) n
Tactic:
simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]
Proof state after:
case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ a = fun n => ε (a n)
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a.hy
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
⊢ ⇑ε ∘ a = fun n => ε (a n)
Tactic:
ext
Proof state after:
case a.hy.h
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
x✝ : σ
⊢ (⇑ε ∘ a) x✝ = ε (a x✝)
Theorem: MvPowerSeries.comp_aeval
Proof state before:
case a.hy.h
σ : Type u_1
inst✝²¹ : DecidableEq σ
R : Type u_2
inst✝²⁰ : CommRing R
inst✝¹⁹ : UniformSpace R
inst✝¹⁸ : UniformAddGroup R
inst✝¹⁷ : TopologicalRing R
S : Type u_3
inst✝¹⁶ : CommRing S
inst✝¹⁵ : UniformSpace S
inst✝¹⁴ : UniformAddGroup S
inst✝¹³ : TopologicalRing S
inst✝¹² : T2Space S
inst✝¹¹ : CompleteSpace S
φ : R →+* S
hφ : Continuous ⇑φ
hS : LinearTopology S
a : σ → S
ha : EvalDomain a
f : MvPowerSeries σ R
d : σ →₀ ℕ
inst✝¹⁰ : Algebra R S
inst✝⁹ : ContinuousSMul R S
T : Type u_4
inst✝⁸ : CommRing T
inst✝⁷ : UniformSpace T
inst✝⁶ : UniformAddGroup T
inst✝⁵ : LinearTopology T
inst✝⁴ : T2Space T
inst✝³ : TopologicalRing T
inst✝² : Algebra R T
inst✝¹ : ContinuousSMul R T
inst✝ : CompleteSpace T
ε : S →ₐ[R] T
hε : Continuous ⇑ε
x✝ : σ
⊢ (⇑ε ∘ a) x✝ = ε (a x✝)
Tactic:
rfl
Proof state after:
no goals
Theorem: MvPolynomial.rTensorAlgHom_coeff_tmul
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d (rTensorAlgHom (p ⊗ₜ[R] n)) = coeff d p ⊗ₜ[R] n
Tactic:
rw [rTensorAlgHom, Algebra.TensorProduct.lift_tmul]
Proof state after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        ((IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))).comp Algebra.TensorProduct.includeRight) n) =
    coeff d p ⊗ₜ[R] n
Theorem: MvPolynomial.rTensorAlgHom_coeff_tmul
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        ((IsScalarTower.toAlgHom R (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))).comp Algebra.TensorProduct.includeRight) n) =
    coeff d p ⊗ₜ[R] n
Tactic:
rw [AlgHom.coe_comp, IsScalarTower.coe_toAlgHom', Function.comp_apply,
  Algebra.TensorProduct.includeRight_apply]
Proof state after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) =
    coeff d p ⊗ₜ[R] n
Theorem: MvPolynomial.rTensorAlgHom_coeff_tmul
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ coeff d
      ((mapAlgHom Algebra.TensorProduct.includeLeft) p *
        (algebraMap (S ⊗[R] N) (MvPolynomial σ (S ⊗[R] N))) (1 ⊗ₜ[R] n)) =
    coeff d p ⊗ₜ[R] n
Tactic:
rw [algebraMap_eq, mul_comm, coeff_C_mul]
Proof state after:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ 1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n
Theorem: MvPolynomial.rTensorAlgHom_coeff_tmul
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
p : MvPolynomial σ S
n : N
d : σ →₀ ℕ
⊢ 1 ⊗ₜ[R] n * coeff d ((mapAlgHom Algebra.TensorProduct.includeLeft) p) = coeff d p ⊗ₜ[R] n
Tactic:
simp [mapAlgHom, coeff_map]
Proof state after:
no goals
Theorem: MvPolynomial.rTensorAlgHom_toLinearMap
Proof state before:
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
⊢ rTensorAlgHom.toLinearMap = ↑(finsuppLeft' R S N (σ →₀ ℕ) S)
Tactic:
ext d n e
Proof state after:
case a.h.h.h.a
R : Type u
M : Type v
N : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
σ : Type u_1
inst✝⁴ : DecidableEq σ
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring N
inst✝ : Algebra R N
d : σ →₀ ℕ
n : N
e : σ →₀ ℕ
⊢ coeff e (((AlgebraTensorModule.curry rTensorAlgHom.toLinearMap ∘ₗ monomial d) 1) n) =
    coeff e (((AlgebraTensorModule.curry ↑(finsuppLeft' R S N (σ →₀ ℕ) S) ∘ₗ monomial d) 1) n)