English
For pb and any y with hy, the linear combination of powers of y representing pb.gen satisfies the equality with aeval; i.e., pb.basis.constr A (i ↦ y^i) (aeval pb.gen f) = aeval y f for any polynomial f.
Русский
Для pb и любого y при условии hy линейная комбинация степеней y, соответствующая pb.gen, удовлетворяет равенству с aeval: pb.basis.constr A (i ↦ y^i) (aeval pb.gen f) = aeval y f для любого полинома f.
LaTeX
$$$ pb.basis.constr A (\lambda i. y^{i}) (\operatorname{aeval}_{pb.gen} f) = \operatorname{aeval}_y f \quad \text{for all } f \in A[X]$$$
Lean4
theorem constr_pow_aeval (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (f : A[X]) :
pb.basis.constr A (fun i => y ^ (i : ℕ)) (aeval pb.gen f) = aeval y f :=
by
cases subsingleton_or_nontrivial A
· rw [(Subsingleton.elim _ _ : f = 0), aeval_zero, map_zero, aeval_zero]
rw [← aeval_modByMonic_eq_self_of_root (minpoly.monic pb.isIntegral_gen) (minpoly.aeval _ _), ←
@aeval_modByMonic_eq_self_of_root _ _ _ _ _ f _ (minpoly.monic pb.isIntegral_gen) y hy]
by_cases hf : f %ₘ minpoly A pb.gen = 0
· simp only [hf, map_zero]
have : (f %ₘ minpoly A pb.gen).natDegree < pb.dim :=
by
rw [← pb.natDegree_minpoly]
apply natDegree_lt_natDegree hf
exact degree_modByMonic_lt _ (minpoly.monic pb.isIntegral_gen)
rw [aeval_eq_sum_range' this, aeval_eq_sum_range' this, map_sum]
refine Finset.sum_congr rfl fun i (hi : i ∈ Finset.range pb.dim) => ?_
rw [Finset.mem_range] at hi
rw [LinearMap.map_smul]
congr
rw [← Fin.val_mk hi, ← pb.basis_eq_pow ⟨i, hi⟩, Basis.constr_basis]
