Ideals_Containing_Ideal_Form_Lattice

Proved

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

idealslatticeproofwikiring-theory

Let $J$ be an ideal of a ring $R$ . Let $\mathbb L_J$ be the set of all ideal of $R$ which contain $J$ . Then the ordered set $\struct {\mathbb L_J, \subseteq}$ is a lattice.

Preamble

import Mathlib.Analysis.Complex.Basic
import Mathlib.RingTheory.Ideal.Basic

Formal statement

theorem Ideals_Containing_Ideal_Form_Lattice {R : Type _} [CommRing R] (J : Ideal R) : ∀ I₁ I₂ : Ideal R, J ≤ I₁ → J ≤ I₂ → J ≤ I₁ ⊓ I₂ := by sorry

Source

https://proofwiki.org/wiki/Ideals_Containing_Ideal_Form_Lattice

View graph