map_eq_zero_of_not_injective — Mathlib

English

If the input map v is not injective, the alternating map evaluated at v is zero.

Русский

Если входная карта не инъективна, значение чередующего отображения на v равно нулю.

LaTeX

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

Lean4

theorem map_eq_zero_of_not_injective (v : ι → M) (hv : ¬Function.Injective v) : f v = 0 :=
  by
  rw [Function.Injective] at hv
  push_neg at hv
  rcases hv with ⟨i₁, i₂, heq, hne⟩
  exact f.map_eq_zero_of_eq v heq hne

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