case empty
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.467150
inst✝¹⁵ : Monoid R'
R'' : Type ?u.467156
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.467168
Q : Type ?u.467171
S : Type ?u.467174
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
m : M
α : Type u_1
n : α → N
⊢ m ⊗ₜ[R] ∑ a in ∅, n a = ∑ a in ∅, m ⊗ₜ[R] n a

case insert
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.467150
inst✝¹⁵ : Monoid R'
R'' : Type ?u.467156
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.467168
Q : Type ?u.467171
S : Type ?u.467174
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
m : M
α : Type u_1
n : α → N
a : α
s : Finset α
has : ¬a ∈ s
ih : m ⊗ₜ[R] ∑ a in s, n a = ∑ a in s, m ⊗ₜ[R] n a
⊢ m ⊗ₜ[R] ∑ a in insert a s, n a = ∑ a in insert a s, m ⊗ₜ[R] n a
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.467150
inst✝¹⁵ : Monoid R'
R'' : Type ?u.467156
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.467168
Q : Type ?u.467171
S : Type ?u.467174
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
m : M
α : Type u_1
s : Finset α
n : α → N
⊢ m ⊗ₜ[R] ∑ a in s, n a = ∑ a in s, m ⊗ₜ[R] n a
induction' s using Finset.induction with a s has ih h
no goals
case empty
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.467150
inst✝¹⁵ : Monoid R'
R'' : Type ?u.467156
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.467168
Q : Type ?u.467171
S : Type ?u.467174
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
m : M
α : Type u_1
n : α → N
⊢ m ⊗ₜ[R] ∑ a in ∅, n a = ∑ a in ∅, m ⊗ₜ[R] n a
simp
no goals
case insert
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.467150
inst✝¹⁵ : Monoid R'
R'' : Type ?u.467156
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.467168
Q : Type ?u.467171
S : Type ?u.467174
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : Module R M
inst✝⁷ : Module R N
inst✝⁶ : Module R P
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : DistribMulAction R' M
inst✝² : Module R'' M
inst✝¹ : SMulCommClass R R' M
inst✝ : SMulCommClass R R'' M
m : M
α : Type u_1
n : α → N
a : α
s : Finset α
has : ¬a ∈ s
ih : m ⊗ₜ[R] ∑ a in s, n a = ∑ a in s, m ⊗ₜ[R] n a
⊢ m ⊗ₜ[R] ∑ a in insert a s, n a = ∑ a in insert a s, m ⊗ₜ[R] n a
simp [Finset.sum_insert has, tmul_add, ih]