Intersection_of_All_Division_Subrings_is_Prime_Subfield

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

division-ringfield-theoryprime-subfieldproofwiki

Let $\struct {K, +, \circ}$ be a division ring. Let $P$ be the intersection of the set of all division subrings of $K$ . Then $P$ is the prime subfield of $K$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Intersection_of_All_Division_Subrings_is_Prime_Subfield {K : Type _} [Field K] : ∃ P : Subfield K, ∀ Q : Subfield K, P ≤ Q := by sorry

Source

https://proofwiki.org/wiki/Intersection_of_All_Division_Subrings_is_Prime_Subfield

View graph