Theorems · Theorem · linear algebra

MultilinearMap.freeFinsuppEquiv_def

∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {κ : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : Fintype ι]
  [inst_2 : CommSemiring R] [inst_3 : DecidableEq R] [inst_4 : DecidableEq ι'] [inst_5 : (i : ι) → Fintype (κ i)]
  [inst_6 : (i : ι) → DecidableEq (κ i)] (f : ((i : ι) → κ i) × ι' →₀ R),
  MultilinearMap.freeFinsuppEquiv f =
    (LinearEquiv.multilinearMapCongrLeft fun x => finsuppLequivDFinsupp R)
      ((LinearEquiv.multilinearMapCongrRight R (finsuppLequivDFinsupp R)).symm
        (MultilinearMap.freeDFinsuppEquiv ((finsuppLequivDFinsupp R) f)))

Defined in

Mathlib.LinearAlgebra.Multilinear.Finsupp

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommSemiringDecidableEqDecidableEqFintypeDecidableEq