English
An arbitrary choice of a root of X^n − C a in the splitting field L of X^n − C a over K is denoted by rootOfSplitsXPowSubC hn a L, where hn: 0 < n.
Русский
Произвольный выбор корня из X^n − C a в разворачивающем поле L над K обозначается как rootOfSplitsXPowSubC hn a L, где hn: 0 < n.
LaTeX
$$$\text{Let } hn>0, \ a \in K, \ L/ K \text{ be a splitting field of } X^n - C a. \text{ Then } \text{rootOfSplitsXPowSubC}(hn) \in L \text{ satisfies } (\text{rootOfSplitsXPowSubC}(hn))^n = a.$$$
Lean4
/-- An arbitrary choice of `ⁿ√a` in the splitting field of `Xⁿ - a`. -/
noncomputable abbrev rootOfSplitsXPowSubC (hn : 0 < n) (a : K) (L) [Field L] [Algebra K L]
[IsSplittingField K L (X ^ n - C a)] : L :=
(rootOfSplits _ (IsSplittingField.splits L (X ^ n - C a))
(by simpa [degree_X_pow_sub_C hn] using Nat.pos_iff_ne_zero.mp hn))
