eval₂ — Mathlib

English

minpoly evaluated via eval₂' equals the same zero relation as eval₂.

Русский

Оценка minpoly через eval₂' даёт тот же нулевой результат, что eval₂.

LaTeX

$$$ \\mathrm{FixedPoints.minpoly}.eval₂'(G\\,F) = 0 $$$

Lean4

theorem eval₂ : Polynomial.eval₂ (Subring.subtype <| (FixedPoints.subfield G F).toSubring) x (minpoly G F x) = 0 :=
  by
  rw [← prodXSubSMul.eval G F x, Polynomial.eval₂_eq_eval_map]
  simp only [minpoly, Polynomial.map_toSubring]

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