minpolyGen — Mathlib

English

The polynomial minpolyGen pb is a polynomial in A[X] given by X^dim minus the linear combination of powers of pb.gen expressed via the pb.basis.

Русский

Полином minpolyGen pb — это полином над A в переменной X, равный X^{dim} минус сумма коэффициентов pb.basis-repr pb.gen^{dim} выраженных через PB-представление.

LaTeX

$$$\text{minpolyGen}(pb) = X^{pb.dim} - \sum_{i=0}^{pb.dim-1} C\big( pb.basis.repr( pb.gen^{pb.dim})_i \big) \; X^{i}$$$

Lean4

/-- `pb.minpolyGen` is the minimal polynomial for `pb.gen`. -/
noncomputable def minpolyGen (pb : PowerBasis A S) : A[X] :=
  X ^ pb.dim - ∑ i : Fin pb.dim, C (pb.basis.repr (pb.gen ^ pb.dim) i) * X ^ (i : ℕ)

Похожие утверждения