Theorems · Theorem · linear algebra

exteriorPower.pairingDual_apply_apply_eq_one_zero

∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_3}
  [inst_3 : LinearOrder ι] (x : ι → M) (f : ι → Module.Dual R M),
  (∀ ⦃i j : ι⦄, i ≠ j → (f i) (x j) = 0) →
    ∀ (n : ℕ) (a b : Fin n ↪o ι),
      a ≠ b →
        ((exteriorPower.pairingDual R M n) ((exteriorPower.ιMulti R n) (f ∘ ⇑a)))
            ((exteriorPower.ιMulti R n) (x ∘ ⇑b)) =
          0

Defined in

Mathlib.LinearAlgebra.ExteriorPower.Pairing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleLinearOrder