-
Notifications
You must be signed in to change notification settings - Fork 330
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat(NumberField/CanonicalEmbedding): define the plusPart
of a set
#18231
base: master
Are you sure you want to change the base?
Conversation
PR summary 69aabc2248Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Let `s` be a set of real places of the number field `K`. This PR defines the map `negAt s` on `mixedSpace K` that swaps the sign at all real places in `s` and proves some of its properties. It will be used later in #18231. This PR is part of the proof of the Analytic Class Number Formula.
This PR/issue depends on: |
Let
A
be a subset of themixedSpace K
of a number fieldK
. We say thatA
is symmetric at real places if it satisfies:∀ x, x ∈ A ↔ (fun w ↦ |x.1 w|, x.2) ∈ A
If
A
is measurable and symmetric at real places, we prove thatwhere
plusPart
is the subset of elements ofA
that are positive at all real places.This PR is part of the proof of the Analytic Class Number Formula.
negAt
map #18234