English
For a field K and a polynomial f ∈ K[x], the splitting field f carries a natural field structure extending K; in particular SplittingField f is a field.
Русский
Для поля K и многочлена f ∈ K[x] развертывающее поле f имеет естественную структуру поля над K; то есть SplittingField f является полем.
LaTeX
$$$\operatorname{Field}(\mathrm{SplittingField}(f))$$$
Lean4
instance instField : Field (SplittingField f)
where
__ := inferInstanceAs <| CommRing (SplittingField f)
__ := instGroupWithZero f
nnratCast q := algebraMap K _ q
ratCast q := algebraMap K _ q
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast_def q := by change algebraMap K _ _ = _; simp_rw [NNRat.cast_def, map_div₀, map_natCast]
ratCast_def q := by change algebraMap K _ _ = _; rw [Rat.cast_def, map_div₀, map_intCast, map_natCast]
nnqsmul_def q
x :=
Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' <| by ext; simp [MvPolynomial.algebraMap_eq, NNRat.smul_def]
qsmul_def q
x :=
Quotient.inductionOn x fun p ↦ congr_arg Quotient.mk'' <| by ext; simp [MvPolynomial.algebraMap_eq, Rat.smul_def]
