Theorems · Theorem · linear algebra

MultilinearMap.pi_ext_iff

∀ {ι : 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},
  f = g ↔
    ∀ (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)

Defined in

Mathlib.LinearAlgebra.Multilinear.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleFiniteFiniteDecidableEq