Commit 2024-01-20 09:50 df8fb034

feat: Prove some results on bases of fractional ideals of number fields (#9836)

• Add the instances that fractional ideals of number fields are finite and free $\mathbb{Z}$-modules
• For I : (FractionalIdeal (𝓞 K)⁰ K)ˣ with K a number field, define a basis of K that spans I over $\mathbb{Z}$
• Prove that the determinant of that basis over an integral basis of K is the absolute norm of I