English
The degree of the i-th Lagrange basis equals card(s) − 1 (as a natural number).
Русский
Степень i-го базиса Лагранжа равна card(s) − 1 (как натуральное число).
LaTeX
$$(\deg L_s,v,i) = |s|-1$$
Lean4
@[simp]
theorem natDegree_basis (hvs : Set.InjOn v s) (hi : i ∈ s) : (Lagrange.basis s v i).natDegree = #s - 1 :=
by
have H : ∀ j, j ∈ s.erase i → basisDivisor (v i) (v j) ≠ 0 :=
by
simp_rw [Ne, mem_erase, basisDivisor_eq_zero_iff]
exact fun j ⟨hij₁, hj⟩ hij₂ => hij₁ (hvs hj hi hij₂.symm)
rw [← card_erase_of_mem hi, card_eq_sum_ones]
convert natDegree_prod _ _ H using 1
refine sum_congr rfl fun j hj => (natDegree_basisDivisor_of_ne ?_).symm
rw [Ne, ← basisDivisor_eq_zero_iff]
exact H _ hj
