case empty
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.457403
inst✝¹⁵ : Monoid R'
R'' : Type ?u.457409
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.457421
Q : Type ?u.457424
S : Type ?u.457427
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
α : Type u_1
m : α → M
n : N
⊢ (∑ a in ∅, m a) ⊗ₜ[R] n = ∑ a in ∅, m a ⊗ₜ[R] n

case insert
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.457403
inst✝¹⁵ : Monoid R'
R'' : Type ?u.457409
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.457421
Q : Type ?u.457424
S : Type ?u.457427
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
α : Type u_1
m : α → M
n : N
a : α
s : Finset α
has : ¬a ∈ s
ih : (∑ a in s, m a) ⊗ₜ[R] n = ∑ a in s, m a ⊗ₜ[R] n
⊢ (∑ a in insert a s, m a) ⊗ₜ[R] n = ∑ a in insert a s, m a ⊗ₜ[R] n
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.457403
inst✝¹⁵ : Monoid R'
R'' : Type ?u.457409
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.457421
Q : Type ?u.457424
S : Type ?u.457427
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
α : Type u_1
s : Finset α
m : α → M
n : N
⊢ (∑ a in s, m a) ⊗ₜ[R] n = ∑ a in s, m a ⊗ₜ[R] n
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.457403
inst✝¹⁵ : Monoid R'
R'' : Type ?u.457409
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.457421
Q : Type ?u.457424
S : Type ?u.457427
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
α : Type u_1
m : α → M
n : N
⊢ (∑ a in ∅, m a) ⊗ₜ[R] n = ∑ a in ∅, m a ⊗ₜ[R] n
simp
no goals
case insert
R : Type u_4
inst✝¹⁶ : CommSemiring R
R' : Type ?u.457403
inst✝¹⁵ : Monoid R'
R'' : Type ?u.457409
inst✝¹⁴ : Semiring R''
M : Type u_2
N : Type u_3
P : Type ?u.457421
Q : Type ?u.457424
S : Type ?u.457427
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
α : Type u_1
m : α → M
n : N
a : α
s : Finset α
has : ¬a ∈ s
ih : (∑ a in s, m a) ⊗ₜ[R] n = ∑ a in s, m a ⊗ₜ[R] n
⊢ (∑ a in insert a s, m a) ⊗ₜ[R] n = ∑ a in insert a s, m a ⊗ₜ[R] n
simp [Finset.sum_insert has, add_tmul, ih]