Theorem Int.ideal_span_absNorm_eq_self

Modification history

2025-05-16 09:35
Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
feat(RingTheory/Ideal): An ideal of `ℤ` is generated by its norm (#24933) …
Added Int.ideal_span_absNorm_eq_selfView on Github →