Commit 2026-05-25 14:55 81749332
View on Github →feat: elements of Dedekind domain approximate elements of valuation ring (#37523)
Algebra part of showing that R is dense in O_v which is used to show that R / v is isomorphic to
the residue field of O_v and construct the base change isomorphism for finite adeles.