Ideals_of_Division_Ring

Proved

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

ideal-theoryproofwiki

Let $\struct {R, +, \circ}$ be a division ring whose zero is $0_R$ . The only ideals of $\struct {R, +, \circ}$ are $\set {0_R}$ and $R$ itself. That is, $\struct {R, +, \circ}$ has no non-null proper ideals.

Preamble

import Mathlib.RingTheory.Ideal.Basic
import Mathlib.Algebra.Field.Basic

Formal statement

theorem Ideals_of_Division_Ring {F : Type _} [Field F] (I : Ideal F) : I = ⊥ ∨ I = ⊤ := by sorry

Source

https://proofwiki.org/wiki/Ideals_of_Division_Ring

View graph