map_eq_zero_of_eq

Mathlib.Topology.Algebra.Module.Alternating.Basic

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

English

If the input v is not injective, then f(v) = 0.

Русский

Если вход не инъективен, то f(v) = 0.

LaTeX

$$$\\neg (\\text{Injective}(v)) \\Rightarrow f(v)=0$$$

Lean4

theorem map_eq_zero_of_eq (v : ι → M) {i j : ι} (h : v i = v j) (hij : i ≠ j) : f v = 0 :=
  f.map_eq_zero_of_eq' v i j h hij

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

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

Разделы

Аффилиация

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