autAdjoinRootXPowSubC_root — Mathlib

English

If an irreducible polynomial defines a normal extension with a primitive root of unity, the associated equiv keeps root fixed up to the unit action.

Русский

Если ирредуцируемый многочлен задаёт нормальное расширение с примитивным корнем единицы, соответствующее эквиз обеспечивает фиксацию корня до действия единицы.

LaTeX

$$$autAdjoinRootXPowSubCEquiv\\; hζ\\; H\\; η\\; (root) = (η^{} : K^\\times) \\, (root)$$$

Lean4

theorem autAdjoinRootXPowSubC_root (η) : autAdjoinRootXPowSubC n a η (root _) = ((η : Kˣ) : K) • root _ :=
  by
  dsimp [autAdjoinRootXPowSubC, autAdjoinRootXPowSubCHom, AlgEquiv.algHomUnitsEquiv]
  apply liftHom_root

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