fractional ideals and orders in a # field as lattices

Stream: Is there code for X?

[Jz Pan]

We have theory of fractional ideals of a number field in mathlib. Seems that we don't have orders in a number field yet. We have a PR #19902 for lattices, but so far it mainly concerns them over PID. Do we have plan to state the properties of lattices over a Dedekind domain (maybe more general), and state some theory of fractional ideals and orders using lattices?