norm): add ideal.finite_set_of_abs_norm_eq (#18569)

Commit

2 years ago

feat(ring_theory/ideal/norm): add ideal.finite_set_of_abs_norm_eq (#18569) Prove that there are only finitely many ideals of `abs_norm` equal to $n$ for $n$ positive.

Author

xroblot

Parents

98bbc352

mathlib3 d3acee0d - feat(ring_theory/ideal/norm): add ideal.finite_set_of_abs_norm_eq (#18569)

mathlib3
d3acee0d - feat(ring_theory/ideal/norm): add ideal.finite_set_of_abs_norm_eq (#18569)