Theorems · Theorem · linear algebra

AlternatingMap.domCoprod.summand_eq_zero_of_smul_invariant

∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4}
  {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁]
  [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ]
  [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂)
  (σ : Equiv.Perm.ModSumCongr ιa ιb) {v : ιa ⊕ ιb → Mᵢ} {i j : ιa ⊕ ιb},
  v i = v j → i ≠ j → Equiv.swap i j • σ = σ → (AlternatingMap.domCoprod.summand a b σ) v = 0

Swapping elements in σ with equal values in v result in zero if the swap has no effect on the quotient.

Defined in

Mathlib.LinearAlgebra.Alternating.DomCoprod

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintypeCommSemiringAddCommGroupModuleAddCommGroupModuleAddCommMonoidModuleDecidableEqDecidableEq