adjoinRootEquivAdjoin_apply_root — Mathlib

English

Under the isomorphism adjoinRootEquivAdjoin F h, the image of AdjoinRoot.root (minpoly F α) is AdjoinSimple.gen F α.

Русский

При отображении через изоморфизм adjoinRootEquivAdjoin F h образ корняAdjoinRoot.root(minpoly F α) совпадает с AdjoinSimple.gen F α.

LaTeX

$$$adjoinRootEquivAdjoin F h (\operatorname{AdjoinRoot.root}(\minpoly F \alpha)) = \operatorname{AdjoinSimple.gen} F \alpha$$$

Lean4

theorem adjoinRootEquivAdjoin_apply_root (h : IsIntegral F α) :
    adjoinRootEquivAdjoin F h (AdjoinRoot.root (minpoly F α)) = AdjoinSimple.gen F α :=
  AdjoinRoot.lift_root (aeval_gen_minpoly F α)

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