Theorems · Theorem · linear algebra

MultilinearMap.dfinsupp_ext_iff

∀ {ι : 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},
  f = g ↔
    ∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => DFinsupp.lsingle (p i)) = g.compLinearMap fun i => DFinsupp.lsingle (p i)

Defined in

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

FiniteSemiringAddCommMonoidAddCommMonoidModuleModuleDecidableEq