Theorems · Theorem · linear algebra

MultilinearMap.dfinsupp_ext

∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [Finite ι]
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)] [inst_2 : AddCommMonoid N]
  [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)] [inst_4 : Module R N] [inst_5 : (i : ι) → DecidableEq (κ i)]
  ⦃f g : MultilinearMap R (fun i => Π₀ (j : κ i), M i j) N⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DFinsupp.lsingle (p i)) = g.compLinearMap fun i => DFinsupp.lsingle (p i)) →
    f = g

Two multilinear maps from finitely supported functions are equal if they agree on the generators. This is a multilinear version of DFinsupp.lhom_ext'.

Defined in

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Cited by

2 results in Mathlib

Foundations

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

Assumes

FiniteSemiringAddCommMonoidAddCommMonoidModuleModuleDecidableEq