English
If y ≠ x then the product over y vanishes.
Русский
Если y ≠ x, то произведение по y обращается в ноль.
LaTeX
$$$\\forall {x y : (π C (· ∈ s))} (h : y \\neq x) : (factors C s x).prod y = 0$$$
Lean4
theorem factors_prod_eq_basis_of_ne {x y : (π C (· ∈ s))} (h : y ≠ x) : (factors C s x).prod y = 0 :=
by
rw [list_prod_apply (π C (· ∈ s)) y _]
apply List.prod_eq_zero
simp only [List.mem_map]
obtain ⟨a, ha⟩ : ∃ a, y.val a ≠ x.val a := by contrapose! h; ext; apply h
cases hx : x.val a
· rw [hx, ne_eq, Bool.not_eq_false] at ha
refine ⟨1 - (e (π C (· ∈ s)) a), ⟨one_sub_e_mem_of_false _ _ ha hx, ?_⟩⟩
rw [e, LocallyConstant.evalMonoidHom_apply, LocallyConstant.sub_apply, LocallyConstant.coe_one, Pi.one_apply,
LocallyConstant.coe_mk, if_pos ha, sub_self]
· refine ⟨e (π C (· ∈ s)) a, ⟨e_mem_of_eq_true _ _ hx, ?_⟩⟩
rw [hx] at ha
rw [LocallyConstant.evalMonoidHom_apply, e, LocallyConstant.coe_mk, if_neg ha]
