Theorems · Theorem · linear algebra

Module.Basis.ext_alternating

∀ {ι : Type u_7} {ι₁ : Type u_10} [Finite ι] {R' : Type u_11} {N₁ : Type u_12} {N₂ : Type u_13} [inst : CommSemiring R']
  [inst_1 : AddCommMonoid N₁] [inst_2 : AddCommMonoid N₂] [inst_3 : Module R' N₁] [inst_4 : Module R' N₂]
  {f g : N₁ [⋀^ι]→ₗ[R'] N₂} (e : Module.Basis ι₁ R' N₁),
  (∀ (v : ι → ι₁), Function.Injective v → (f fun i => e (v i)) = g fun i => e (v i)) → f = g

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

Defined in

Mathlib.LinearAlgebra.Alternating.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FiniteCommSemiringAddCommMonoidAddCommMonoidModuleModule