map_mk

Mathlib.Algebra.Category.ModuleCat.ExteriorPower

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

← MathLib Explorer

English

The action of map on generators is given by map f n (mk x) = mk (f ∘ x).

Русский

Действие map на генераторах: map f n (mk x) = mk (f ∘ x).

LaTeX

$$map f n (mk x) = mk (f ∘ x)$$

Lean4

@[simp]
theorem map_mk {M N : ModuleCat.{v} R} (f : M ⟶ N) {n : ℕ} (x : Fin n → M) : map f n (mk x) = mk (f ∘ x) := by
  apply exteriorPower.map_apply_ιMulti

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

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

Разделы

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

Аффилиация

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