postcomp

Mathlib.Algebra.Category.ModuleCat.ExteriorPower

URI: https://scilib.ai/kg/mathlib#ModuleCat.AlternatingMap.postcomp

English

The morphism desc φ applied to the generator mk x yields φ x.

Русский

Отображение desc φ на элемент mk x даёт φ x.

LaTeX

$$desc φ (mk x) = φ x$$

Lean4

/-- The postcomposition of an alternating map by a linear map. -/
def postcomp : M.AlternatingMap N' n :=
  g.hom.compAlternatingMap φ

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru