Theorem Ideal.exists_isMaximal_dvd_of_dvd_absNorm

Modification history

2026-05-07 17:04
Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
feat(NumberTheory): every number field has a ramified prime (#30666)
Added Ideal.exists_isMaximal_dvd_of_dvd_absNormView on Github →