finrank_of_isSplittingField_X_pow_sub_C

English

For L/K as a splitting field of X^n − C a, the degree [L:K] equals n.

Русский

Для L/K как разворачивающего поля X^n − C a степень разложения равна n.

LaTeX

$$$[L:K] = n$$$

Lean4

theorem finrank_of_isSplittingField_X_pow_sub_C : Module.finrank K L = n :=
  by
  have := Polynomial.IsSplittingField.finiteDimensional L (X ^ n - C a)
  have := isGalois_of_isSplittingField_X_pow_sub_C hζ H L
  have hn := Nat.pos_iff_ne_zero.mpr (ne_zero_of_irreducible_X_pow_sub_C H)
  have : NeZero n := ⟨ne_zero_of_irreducible_X_pow_sub_C H⟩
  rw [← IsGalois.card_aut_eq_finrank,
    Nat.card_congr ((autEquivZmod H L <| (mem_primitiveRoots hn).mp hζ.choose_spec).toEquiv.trans Multiplicative.toAdd),
    Nat.card_zmod]

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