eval_indicator_apply_eq_zero — Mathlib

English

For any a,b: σ → K with a ≠ b, the evaluation of indicator(b) at a is zero: eval(a)(indicator(b)) = 0.

Русский

Пусть a, b: σ → K и a ≠ b. Тогда подстановка a в индикатор-indicator(b) даёт 0: eval(a)(indicator(b)) = 0.

LaTeX

$$$\\\\mathrm{eval}(a,\\\\mathrm{indicator}(b)) = 0 \\\\text{ if } a \\\\neq b$$$

Lean4

theorem eval_indicator_apply_eq_zero (a b : σ → K) (h : a ≠ b) : eval a (indicator b) = 0 :=
  by
  obtain ⟨i, hi⟩ : ∃ i, a i ≠ b i := by rwa [Ne, funext_iff, not_forall] at h
  simp only [indicator, map_prod, map_sub, map_one, map_pow, eval_X, eval_C, Finset.prod_eq_zero_iff]
  refine ⟨i, Finset.mem_univ _, ?_⟩
  rw [FiniteField.pow_card_sub_one_eq_one, sub_self]
  rwa [Ne, sub_eq_zero]

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