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✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁶ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  ↑f (Finset.piecewise (Finset.erase Finset.univ i) (c • update m i x) (update m i x)) =
    (∏ _i in Finset.erase Finset.univ i, c) • ↑f (update m i x)
⊢ ↑f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • ↑f (update m i x)
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✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁶ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
⊢ ↑f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • ↑f (update m i x)
have :
  f ((Finset.univ.erase i).piecewise (c • update m i x) (update m i x)) =
    (∏ _i in Finset.univ.erase i, c) • f (update m i x) :=
  map_piecewise_smul f _ _ _
no goals
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✝⁸ : CommSemiring R
inst✝⁷ : (i : ι) → AddCommMonoid (M₁ i)
inst✝⁶ : (i : Fin (Nat.succ n)) → AddCommMonoid (M i)
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : (i : Fin (Nat.succ n)) → Module R (M i)
inst✝³ : (i : ι) → Module R (M₁ i)
inst✝² : Module R M₂
f f' : MultilinearMap R M₁ M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
m : (i : ι) → M₁ i
i : ι
c : R
x : M₁ i
this :
  ↑f (Finset.piecewise (Finset.erase Finset.univ i) (c • update m i x) (update m i x)) =
    (∏ _i in Finset.erase Finset.univ i, c) • ↑f (update m i x)
⊢ ↑f (update (c • m) i x) = c ^ (Fintype.card ι - 1) • ↑f (update m i x)
simpa [← Function.update_smul c m] using this