mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

feat(NumberField/CanonicalEmbedding): define the `negAt` map

Open xroblot opened this issue 1 year ago • 1 comments

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.

Open in Gitpod

xroblot avatar Oct 25 '24 15:10 xroblot