Theorems · Theorem · linear algebra

Module.Basis.ext_multilinear

∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : Type u_4} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Finite ι]
  {f g : MultilinearMap R M N} {ιM : ι → Type u_5} (e : (i : ι) → Module.Basis (ιM i) R (M i)),
  (∀ (v : (i : ι) → ιM i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g

Two multilinear maps indexed by a Fintype are equal if they are equal when all arguments are basis vectors.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleAddCommMonoidModuleFinite