case empty
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
α✝ : ι → Type ?u.279373
g✝ : (i : ι) → α✝ i → M₁ i
A : (i : ι) → Finset (α✝ i)
α : Type u_1
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ ↑f (update m i (∑ a in ∅, g a)) = ∑ a in ∅, ↑f (update m i (g a))

case insert
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
α✝ : ι → Type ?u.279373
g✝ : (i : ι) → α✝ i → M₁ i
A : (i : ι) → Finset (α✝ i)
α : Type u_1
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
a : α
t : Finset α
has : ¬a ∈ t
ih : ↑f (update m i (∑ a in t, g a)) = ∑ a in t, ↑f (update m i (g a))
⊢ ↑f (update m i (∑ a in insert a t, g a)) = ∑ a in insert a t, ↑f (update m i (g a))
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
α✝ : ι → Type ?u.279373
g✝ : (i : ι) → α✝ i → M₁ i
A : (i : ι) → Finset (α✝ i)
α : Type u_1
inst✝ : DecidableEq ι
t : Finset α
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ ↑f (update m i (∑ a in t, g a)) = ∑ a in t, ↑f (update m i (g a))
induction' t using Finset.induction with a t has ih h
no goals
case empty
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
α✝ : ι → Type ?u.279373
g✝ : (i : ι) → α✝ i → M₁ i
A : (i : ι) → Finset (α✝ i)
α : Type u_1
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
⊢ ↑f (update m i (∑ a in ∅, g a)) = ∑ a in ∅, ↑f (update m i (g a))
simp
no goals
case insert
R : Type u
ι : Type u'
n : ℕ
M : Fin (Nat.succ n) → Type v
M₁ : ι → Type v₁
M₂ : Type v₂
M₃ : Type v₃
M' : Type v'
inst✝¹¹ : Semiring R
inst✝¹⁰ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁹ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁸ : AddCommMonoid M₂
inst✝⁷ : AddCommMonoid M₃
inst✝⁶ : AddCommMonoid M'
inst✝⁵ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝⁴ : (i : ι) → Module R (M₁ i)
inst✝³ : Module R M₂
inst✝² : Module R M₃
inst✝¹ : Module R M'
f f' : MultilinearMap R M₁ M₂
α✝ : ι → Type ?u.279373
g✝ : (i : ι) → α✝ i → M₁ i
A : (i : ι) → Finset (α✝ i)
α : Type u_1
inst✝ : DecidableEq ι
i : ι
g : α → M₁ i
m : (i : ι) → M₁ i
a : α
t : Finset α
has : ¬a ∈ t
ih : ↑f (update m i (∑ a in t, g a)) = ∑ a in t, ↑f (update m i (g a))
⊢ ↑f (update m i (∑ a in insert a t, g a)) = ∑ a in insert a t, ↑f (update m i (g a))
simp [Finset.sum_insert has, ih]