English
The algebraic closure AlgebraicClosure(k) carries a field structure, i.e., it is a field.
Русский
Замыкание AlgebraicClosure(k) является полем.
LaTeX
$$$\text{Field}(\text{AlgebraicClosure}(k)).$$$
Lean4
instance instField : Field (AlgebraicClosure k)
where
__ := instCommRing _
__ := instGroupWithZero _
nnqsmul := (· • ·)
qsmul := (· • ·)
nnratCast q := algebraMap k _ q
ratCast q := algebraMap k _ q
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]
