aeval_minpoly_iff — Mathlib

English

For any x, aeval x c.minpoly = 0 if and only if mk K x = c.

Русский

Для любого x выполняется: aeval x c.minpoly = 0 тогда и только тогда mk K x = c.

LaTeX

$$$\\operatorname{aeval}(x, c.minpoly) = 0 \\iff \\operatorname{mk}(K, x) = c$$$

Lean4

theorem aeval_minpoly_iff (x : L) (c : ConjRootClass K L) : aeval x c.minpoly = 0 ↔ mk K x = c :=
  by
  induction c
  simpa [← isConjRoot_iff_aeval_eq_zero (Algebra.IsIntegral.isIntegral _)] using comm

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