minpoly_mk — Mathlib

English

For any x ∈ L, the minimal polynomial of the canonical class mk K x equals the usual minimal polynomial of x: (mk K x).minpoly = minpoly K x.

Русский

Для любого x ∈ L минимальный полином канонического класса mk K x совпадает с обычным минимальным полиномом x: (mk K x).minpoly = minpoly K x.

LaTeX

$$$(\\mathrm{mk}\\ K\ \, x).minpoly = \\minpoly\ K\ x$$$

Lean4

@[simp]
theorem minpoly_mk (x : L) : (mk K x).minpoly = minpoly K x :=
  rfl

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