English
The construction respects multiplication: pb.basis.constr A (\lambda i. y^i) (x x') = pb.basis.constr A (\lambda i. y^i) x · pb.basis.constr A (\lambda i. y^i) x'.
Русский
Конструкция сохраняет умножение: конструирование от произведения равно произведению конструирования.
LaTeX
$$$ pb.basis.constr A (\lambda i. y^{i}) (x \cdot x') = pb.basis.constr A (\lambda i. y^{i}) x \cdot pb.basis.constr A (\lambda i. y^{i}) x' $$$
Lean4
theorem constr_pow_mul (pb : PowerBasis A S) {y : S'} (hy : aeval y (minpoly A pb.gen) = 0) (x x' : S) :
pb.basis.constr A (fun i => y ^ (i : ℕ)) (x * x') =
pb.basis.constr A (fun i => y ^ (i : ℕ)) x * pb.basis.constr A (fun i => y ^ (i : ℕ)) x' :=
by
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x
obtain ⟨g, rfl⟩ := pb.exists_eq_aeval' x'
simp only [← aeval_mul, pb.constr_pow_aeval hy]
