The ring of integers of a number field K
is free of dimension [K : ℚ]
/ develop the theory of lattices
#18150
Labels
feature-request
This issue is a feature request, either for mathematics, tactics, or CI
good-first-project
t-algebra
Algebra (groups, rings, fields etc)
t-number-theory
Number theory (also use t-algebra or t-analysis to specialize)
Projects
We are absolutely ready to prove this. For example the fact that
𝓞 K
is free overℤ
is very easyBut the correct thing to do is to develop the theory of lattices, proving that a
ℤ
-basis gives also aℚ
-basis. Note that we have basis.localization, but this is the wrong statement, since it take aℤ
-basis ofM
and produces aℚ
-basis ofM
(in practice it only applies in trivial cases).A sketch would be something like (of course one should not use tactic mode for the whole definition)
See this comment for a nice application.
The text was updated successfully, but these errors were encountered: