English
IsSplittingField holds for the splitting field of X^n − C a over K given irreducibility and primitive roots exist.
Русский
IsSplittingField выполняется для разложения корней X^n − C a над K при условии ирредуцируемости и существования примитивных корней.
LaTeX
$$$\\text{IsSplittingField}(K, \\text{AdjoinRoot}(X^n - C a))$$$
Lean4
theorem isSplittingField_AdjoinRoot_X_pow_sub_C :
haveI := Fact.mk H
letI : Algebra K K[n√a] := inferInstance
IsSplittingField K K[n√a] (X ^ n - C a) :=
by
have := Fact.mk H
letI : Algebra K K[n√a] := inferInstance
constructor
· rw [← splits_id_iff_splits, Polynomial.map_sub, Polynomial.map_pow, Polynomial.map_C, Polynomial.map_X]
have ⟨_, hζ⟩ := hζ
rw [mem_primitiveRoots (Nat.pos_of_ne_zero <| ne_zero_of_irreducible_X_pow_sub_C H)] at hζ
exact
X_pow_sub_C_splits_of_isPrimitiveRoot (hζ.map_of_injective (algebraMap K _).injective) (root_X_pow_sub_C_pow n a)
· rw [eq_top_iff, ← AdjoinRoot.adjoinRoot_eq_top]
apply Algebra.adjoin_mono
have := ne_zero_of_irreducible_X_pow_sub_C H
rw [Set.singleton_subset_iff, mem_rootSet_of_ne (X_pow_sub_C_ne_zero (Nat.pos_of_ne_zero this) a), aeval_def,
AdjoinRoot.algebraMap_eq, AdjoinRoot.eval₂_root]
