Theorems · Definition · linear algebra

AlternatingMap.constLinearEquivOfIsEmpty

{ι : Type u_7} →
  {R' : Type u_10} →
    {M'' : Type u_11} →
      {N'' : Type u_13} →
        [inst : CommSemiring R'] →
          [inst_1 : AddCommMonoid M''] →
            [inst_2 : AddCommMonoid N''] →
              [inst_3 : Module R' M''] → [inst_4 : Module R' N''] → [IsEmpty ι] → N'' ≃ₗ[R'] M'' [⋀^ι]→ₗ[R'] N''

The space of constant maps is equivalent to the space of maps that are alternating with respect to an empty family.

Defined in

Mathlib.LinearAlgebra.Alternating.Basic

Cited by

10 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModuleIsEmpty