Theorem Ideal.isMaximal_of_isPrime_of_ne_bot

Modification history

2026-05-07 17:04

Mathlib/RingTheory/KrullDimension/Basic.lean

feat(NumberTheory): every number field has a ramified prime (#30666)

Added Ideal.isMaximal_of_isPrime_of_ne_bot View on Github →