internlm/Lean-Github huggingface dataset:
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5
σ : 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
d : σ →₀ ℕ
hd : ¬d = 0
⊢ (d.prod fun s n => Function.const σ 0 s ^ n) = 0
Tactic:
simp only [DFunLike.ext_iff, Finsupp.coe_zero, Pi.zero_apply, not_forall] at hd
Proof state after:
case h.e'_2.h.e'_5
σ : 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
d : σ →₀ ℕ
hd : ∃ x, ¬d x = 0
⊢ (d.prod fun s n => Function.const σ 0 s ^ n) = 0
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5
σ : 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
d : σ →₀ ℕ
hd : ∃ x, ¬d x = 0
⊢ (d.prod fun s n => Function.const σ 0 s ^ n) = 0
Tactic:
obtain ⟨s, hs⟩ := hd
Proof state after:
case h.e'_2.h.e'_5.intro
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ (d.prod fun s n => Function.const σ 0 s ^ n) = 0
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5.intro
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ (d.prod fun s n => Function.const σ 0 s ^ n) = 0
Tactic:
simp only [Finsupp.prod]
Proof state after:
case h.e'_2.h.e'_5.intro
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ ∏ x ∈ d.support, Function.const σ 0 x ^ d x = 0
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5.intro
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ ∏ x ∈ d.support, Function.const σ 0 x ^ d x = 0
Tactic:
apply Finset.prod_eq_zero (i := s)
Proof state after:
case h.e'_2.h.e'_5.intro.hi
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ s ∈ d.support

case h.e'_2.h.e'_5.intro.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
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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ Function.const σ 0 s ^ d s = 0
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5.intro.hi
σ : 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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ d s ≠ 0

case h.e'_2.h.e'_5.intro.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
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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ Function.const σ 0 s ^ d s = 0
Tactic:
exact hs
Proof state after:
case h.e'_2.h.e'_5.intro.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
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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ Function.const σ 0 s ^ d s = 0
Theorem: MvPowerSeries.scale_zero_apply
Proof state before:
case h.e'_2.h.e'_5.intro.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
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
d : σ →₀ ℕ
s : σ
hs : ¬d s = 0
⊢ Function.const σ 0 s ^ d s = 0
Tactic:
simp only [Function.const_apply, zero_pow hs]
Proof state after:
no goals
Theorem: MvPowerSeries.scale_linear_eq_smul
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
⊢ scale (Function.const σ r) f = r • 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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (coeff R e) (scale (Function.const σ r) f) = (coeff R e) (r • f)
Theorem: MvPowerSeries.scale_linear_eq_smul
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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (coeff R e) (scale (Function.const σ r) f) = (coeff R e) (r • f)
Tactic:
simp only [MvPowerSeries.coeff_scale, map_smul]
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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (e.prod fun s n => Function.const σ r s ^ n) • (coeff R e) f = (coeff R e) (r • f)
Theorem: MvPowerSeries.scale_linear_eq_smul
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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (e.prod fun s n => Function.const σ r s ^ n) • (coeff R e) f = (coeff R e) (r • f)
Tactic:
simp only [Finsupp.prod, Function.const_apply, Finset.prod_pow_eq_pow_sum, smul_eq_mul]
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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Theorem: MvPowerSeries.scale_linear_eq_smul
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
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Tactic:
by_cases he : Finsupp.sum e (fun _ n ↦ n) = 1
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : (e.sum fun x n => n) = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)

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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : ¬(e.sum fun x n => n) = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Theorem: MvPowerSeries.scale_linear_eq_smul
Proof state before:
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : (e.sum fun x n => n) = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)
Tactic:
simp only [Finsupp.sum] at he
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
r : A
f : MvPowerSeries σ R
hf : ∀ (d : σ →₀ ℕ), (d.sum fun x n => n) ≠ 1 → (coeff R d) f = 0
e : σ →₀ ℕ
he : ∑ x ∈ e.support, e x = 1
⊢ (r ^ ∑ i ∈ e.support, e i) • (coeff R e) f = (coeff R e) (r • f)