adjoinRootXPowSubCEquiv_root — Mathlib

English

In the splitting field, the image of the root under adjoinRootXPowSubCEquiv with hα is the chosen root.

Русский

В поле разложения образ корня через adjoinRootXPowSubCEquiv с hα равен выбранному корню.

LaTeX

$$$adjoinRootXPowSubCEquiv\\; hζ\\; H\\; hα\\; (root) = root$$$

Lean4

theorem adjoinRootXPowSubCEquiv_root : adjoinRootXPowSubCEquiv hζ H hα (root _) = α := by
  rw [adjoinRootXPowSubCEquiv, AlgEquiv.coe_ofBijective, liftHom_root]

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