eval_basis_of_ne — Mathlib

English

The natural degree of the i-th Lagrange basis is card(s) − 1 when v is injective on s.

Русский

Естественная степень i-го базиса Лагранжа равна card(s) − 1 при инъективности v на s.

LaTeX

$$(\operatorname{natDegree})(L_s,v,i)=|s|-1$$

Lean4

@[simp]
theorem eval_basis_of_ne (hij : i ≠ j) (hj : j ∈ s) : (Lagrange.basis s v i).eval (v j) = 0 :=
  by
  simp_rw [Lagrange.basis, eval_prod, prod_eq_zero_iff]
  exact ⟨j, ⟨mem_erase.mpr ⟨hij.symm, hj⟩, eval_basisDivisor_right⟩⟩

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