Theorems · Theorem · linear algebra

MultilinearMap.pi_ext

∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : Type uN} [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] [Finite ι] [∀ (i : ι), Finite (κ i)]
  [inst_7 : (i : ι) → DecidableEq (κ i)] ⦃f g : MultilinearMap R (fun i => (j : κ i) → M i j) N⦄,
  (∀ (p : (i : ι) → κ i),
      (f.compLinearMap fun i => LinearMap.single R (M i) (p i)) =
        g.compLinearMap fun i => LinearMap.single R (M i) (p i)) →
    f = g

Two multilinear maps from finite families are equal if they agree on the generators. This is a multilinear version of LinearMap.pi_ext.

Defined in

Mathlib.LinearAlgebra.Multilinear.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleFiniteFiniteDecidableEq