closure_range_algebraMap — Mathlib

English

Let A be a commutative ring with fraction field K. The subfield of K generated by the image of the canonical map algebraMap A K is the entire field K.

Русский

Пусть A — коммутативное кольцо, у которого поля дробей K. Подполье K, порождаемое образом алгебраического отображения algebraMap A K, совпадает с всем полем K.

LaTeX

$$$\operatorname{Subfield.closure}(\operatorname{Set.range}(\operatorname{algebraMap} A K)) = \top$$$

Lean4

/-- If `A` is a commutative ring with fraction field `K`, then the subfield of `K` generated by
the image of `algebraMap A K` is equal to the whole field `K`. -/
theorem closure_range_algebraMap : Subfield.closure (Set.range (algebraMap A K)) = ⊤ :=
  top_unique fun z _ ↦ by
    obtain ⟨_, _, -, rfl⟩ := div_surjective (A := A) z
    apply div_mem <;> exact Subfield.subset_closure ⟨_, rfl⟩

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