Theorems · Definition · linear algebra

ExteriorAlgebra.toTrivSqZeroExt

{R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          [inst_3 : Module Rᵐᵒᵖ M] → [inst_4 : IsCentralScalar R M] → ExteriorAlgebra R M →ₐ[R] TrivSqZeroExt R M

The canonical map from ExteriorAlgebra R M into TrivSqZeroExt R M that sends ExteriorAlgebra.ι to TrivSqZeroExt.inr.

Defined in

Mathlib.LinearAlgebra.ExteriorAlgebra.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModuleModuleIsCentralScalar