norm_gen_eq_coeff_zero_minpoly — Mathlib

English

For a power basis pb with generator g, the norm of g equals (-1)^{dim(pb)} times the constant term of its minimal polynomial.

Русский

Для оснований по степеням pb и генератора g норма g равна (-1)^{dim(pb)} умножить на константный член минимального многочлена g.

LaTeX

$$norm R pb.gen = (-1)^{pb.dim} · coeff (minpoly R pb.gen) 0$$

Lean4

/-- Given `pb : PowerBasis K S`, then the norm of `pb.gen` is
`(-1) ^ pb.dim * coeff (minpoly K pb.gen) 0`. -/
theorem norm_gen_eq_coeff_zero_minpoly (pb : PowerBasis R S) :
    norm R pb.gen = (-1) ^ pb.dim * coeff (minpoly R pb.gen) 0 := by
  rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_leftMulMatrix, Fintype.card_fin]

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