English
For any n < natDegree f, h.coeff(h.root^n) = Pi.single n 1.
Русский
Для любого n < natDegree f, h.coeff(h.root^n) = Pi.single n 1.
LaTeX
$$$ h.coeff\\,(h.root^n) = \\Pi.single\\ n\\ 1 $$$
Lean4
theorem coeff_root_pow {n} (hn : n < natDegree f) : h.coeff (h.root ^ n) = Pi.single n 1 :=
by
ext i
rw [coeff_apply]
split_ifs with hi
·
calc
h.basis.repr (h.root ^ n) ⟨i, _⟩ = h.basis.repr (h.basis ⟨n, hn⟩) ⟨i, hi⟩ := by rw [h.basis_apply, Fin.val_mk]
_ = Pi.single (M := fun _ => R) ((⟨n, hn⟩ : Fin _) : ℕ) (1 : (fun _ => R) n) ↑(⟨i, _⟩ : Fin _) := by
rw [h.basis.repr_self, ← Finsupp.single_eq_pi_single, Finsupp.single_apply_left Fin.val_injective]
_ = Pi.single (M := fun _ => R) n 1 i := by rw [Fin.val_mk, Fin.val_mk]
· rw [Pi.single_eq_of_ne]
rintro rfl
simp [hi] at hn
