Commit 2024-02-09 11:48 3e8b888d
View on Github →feat: Add exists_ideal_in_class_of_norm_le (#9084) Prove that each class of the classgroup of a number field contains an integral ideal of small norm.
feat: Add exists_ideal_in_class_of_norm_le (#9084) Prove that each class of the classgroup of a number field contains an integral ideal of small norm.