Theorems · Definition · linear algebra

ModuleCat.AlternatingMap.postcomp

{R : Type u} →
  [inst : CommRing R] →
    {M : ModuleCat R} →
      {N : ModuleCat R} → {n : ℕ} → M.AlternatingMap N n → {N' : ModuleCat R} → (N ⟶ N') → M.AlternatingMap N' n

The postcomposition of an alternating map by a linear map.

Defined in

Mathlib.Algebra.Category.ModuleCat.ExteriorPower

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRing