Theorems · Theorem · linear algebra

MultilinearMap.domCoprod_alternization_coe

∀ {ι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 : MultilinearMap R' (fun x => Mᵢ) N₁)
  (b : MultilinearMap R' (fun x => Mᵢ) N₂),
  (↑(MultilinearMap.alternatization a)).domCoprod ↑(MultilinearMap.alternatization b) =
    ∑ σa,
      ∑ σb,
        Equiv.Perm.sign σa •
          Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b)

A helper lemma for MultilinearMap.domCoprod_alternization.

Defined in

Mathlib.LinearAlgebra.Alternating.DomCoprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintypeCommSemiringAddCommGroupModuleAddCommGroupModuleAddCommMonoidModuleDecidableEqDecidableEq