English
When applying the algebra evaluation at pb.gen to minpolyGen pb, the result is the zero map: aeval(pb.gen)(minpolyGen(pb)) = 0.
Русский
При применении алгебраического вычисления в pb.gen к minpolyGen pb результат нулевой: aeval(pb.gen)(minpolyGen(pb)) = 0.
LaTeX
$$$\operatorname{aeval}_{pb.gen}\big(\text{minpolyGen}(pb)\big) = 0$$$
Lean4
theorem aeval_minpolyGen (pb : PowerBasis A S) : aeval pb.gen (minpolyGen pb) = 0 :=
by
simp_rw [minpolyGen, map_sub, map_sum, map_mul, map_pow, aeval_C, ← Algebra.smul_def, aeval_X]
refine sub_eq_zero.mpr ((pb.basis.linearCombination_repr (pb.gen ^ pb.dim)).symm.trans ?_)
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype] <;> simp only [pb.coe_basis, zero_smul, imp_true_iff]
