Theorems · Definition · linear algebra

PiTensorProduct.dualDistribInvOfBasis

{ι : Type u_1} →
  {R : Type u_2} →
    {κ : ι → Type u_3} →
      {M : ι → Type u_4} →
        [inst : CommRing R] →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [Finite ι] →
                [∀ (i : ι), Finite (κ i)] →
                  ((i : ι) → Module.Basis (κ i) R (M i)) →
                    Module.Dual R (PiTensorProduct R fun i => M i) →ₗ[R] PiTensorProduct R fun i => Module.Dual R (M i)

An inverse to PiTensorProduct.dualDistrib given bases.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Dual

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleFiniteFinite