Theorems · Theorem · linear algebra

MultilinearMap.domCoprod_alternization_eq

∀ {ι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₂),
  MultilinearMap.alternatization ((↑a).domCoprod ↑b) =
    ((Fintype.card ιa).factorial * (Fintype.card ιb).factorial) • a.domCoprod b

Taking the MultilinearMap.alternatization of the MultilinearMap.domCoprod of two AlternatingMaps gives a scaled version of the AlternatingMap.coprod of those maps.

Defined in

Mathlib.LinearAlgebra.Alternating.DomCoprod

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeFintypeCommSemiringAddCommGroupModuleAddCommGroupModuleAddCommMonoidModuleDecidableEqDecidableEq