desc_mk

Mathlib.Algebra.Category.ModuleCat.ExteriorPower

URI: https://scilib.ai/kg/mathlib#ModuleCat.exteriorPower.desc_mk

← MathLib Explorer

English

The action of desc on mk x yields the underlying φ applied to x.

Русский

Действие desc на mk x даёт φ x.

LaTeX

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

Lean4

@[simp]
theorem desc_mk {M : ModuleCat.{v} R} {n : ℕ} {N : ModuleCat.{max u v} R} (φ : M.AlternatingMap N n) (x : Fin n → M) :
    desc φ (mk x) = φ x := by apply exteriorPower.alternatingMapLinearEquiv_apply_ιMulti

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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