fromZetaAut_spec — Mathlib

English

There is a Galois-type isomorphism for X^n − 1 whose Gal group is isomorphic to (Z/nZ)×, again via the aut-congruence construction.

Русский

Существует изоморфизм Галои для X^n−1, при этом группа Галои изоморфна (Z/nZ)× через соответствующую конструкцию автоматов.

LaTeX

$$$(\text{X}^n - 1)\,\text{Gal} \cong (\mathbb{Z}/n\mathbb{Z})^{\times}$$$

Lean4

theorem fromZetaAut_spec : fromZetaAut hμ h (zeta n K L) = μ :=
  by
  simp_rw [fromZetaAut, autEquivPow_symm_apply]
  generalize_proofs hζ h _ hμ _
  nth_rewrite 4 [← hζ.powerBasis_gen K]
  rw [PowerBasis.equivOfMinpoly_gen, hμ.powerBasis_gen K]
  convert h.choose_spec.2
  exact ZMod.val_cast_of_lt h.choose_spec.1

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