factors_prod_eq_basis_of_eq — Mathlib

English

If x ≠ y in the π-space, then the product over y is 0.

Русский

Если x и y различны в π-пространстве, то произведение по y равно нулю.

LaTeX

$$$\\forall {x y : (π C (· ∈ s))} (h : y ≠ x) : (factors C s x).prod y = 0$$$

Lean4

theorem factors_prod_eq_basis_of_eq {x y : (π C fun x ↦ x ∈ s)} (h : y = x) : (factors C s x).prod y = 1 :=
  by
  rw [list_prod_apply (π C (· ∈ s)) y _]
  apply List.prod_eq_one
  simp only [h, List.mem_map, LocallyConstant.evalMonoidHom, factors]
  rintro _ ⟨a, ⟨b, _, rfl⟩, rfl⟩
  dsimp
  split_ifs with hh
  · rw [e, LocallyConstant.coe_mk, if_pos hh]
  · rw [LocallyConstant.sub_apply, e, LocallyConstant.coe_mk, LocallyConstant.coe_mk, if_neg hh]
    simp only [LocallyConstant.toFun_eq_coe, LocallyConstant.coe_one, Pi.one_apply, sub_zero]

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