map_eq_zero_of_not_injective

Mathlib.Topology.Algebra.Module.Alternating.Basic

URI: https://scilib.ai/kg/mathlib#ContinuousAlternatingMap.map_eq_zero_of_not_injective

English

The scalar action commutes with evaluation: (c•f)(v) = c•f(v).

Русский

Скалярное действие совместимо с применением к функции: (c•f)(v) = c•f(v).

LaTeX

$$$\\forall c,v,\\ (c\\cdot f)(v) = c\\cdot f(v)$$$

Lean4

theorem map_eq_zero_of_not_injective (v : ι → M) (hv : ¬Function.Injective v) : f v = 0 :=
  f.toAlternatingMap.map_eq_zero_of_not_injective v hv

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

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

Разделы

Аффилиация

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