Theorems · Theorem · linear algebra

LinearMap.uncurryMid_apply

∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (p : Fin (n + 1))
  (f : M p →ₗ[R] MultilinearMap R (fun i => M (p.succAbove i)) M₂) (m : (i : Fin n.succ) → M i),
  (LinearMap.uncurryMid p f) m = (f (m p)) (p.removeNth m)

Defined in

Mathlib.LinearAlgebra.Multilinear.Curry

Cited by

3 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule