Theorems · Theorem · linear algebra

MultilinearMap.domCoprod_alternization

∀ {ι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 b) =
    (MultilinearMap.alternatization a).domCoprod (MultilinearMap.alternatization b)

Computing the MultilinearMap.alternatization of the MultilinearMap.domCoprod is the same as computing the AlternatingMap.domCoprod of the MultilinearMap.alternatizations.

Defined in

Mathlib.LinearAlgebra.Alternating.DomCoprod

Cited by

1 results in Mathlib

Foundations

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

Assumes

FintypeFintypeCommSemiringAddCommGroupModuleAddCommGroupModuleAddCommMonoidModuleDecidableEqDecidableEq