Theorem Ideal.IsMaximal.ne_bot_of_isIntegral_int

Modification history

2026-05-07 17:04
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
feat(NumberTheory): every number field has a ramified prime (#30666)
Added Ideal.IsMaximal.ne_bot_of_isIntegral_intView on Github →