Commit 2025-11-28 16:39 d6ab1122

refactor: use isometry extensions for completions at infinite places of number fields (#29969) The API for InfinitePlace.Completion currently makes use of abstract results defined on absolute values, which all depend on the hypothesis of the form ∀ x, ‖f x‖ = v x. This is equivalent to f being an isometry, and so many of these results can be bypassed and deprecated by using Isometry.completion_extension