feat(NumberField/CanonicalEmbedding): define the negAt map

[xroblot]

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.

---

[github-actions]

PR summary b2c24ffa4c

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	2245	2252	+7 (+0.31%)

Import changes for all files

Files	Import difference
3 files Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.NumberTheory.NumberField.House Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic	7

---

Declarations diff

+ coe_neg
+ instance : IsAddHaarMeasure (volume : Measure (mixedSpace K))
+ neg
+ negAt
+ negAt_apply_abs_of_isReal
+ negAt_apply_of_isComplex
+ negAt_apply_of_isReal_and_mem
+ negAt_apply_of_isReal_and_not_mem
+ negAt_apply_snd
+ negAt_signSet_apply_of_isComplex
+ negAt_signSet_apply_of_isReal
+ negAt_symm
+ neg_apply
+ normAtPlace_negAt
+ norm_negAt
+ piCongrRight
+ piCongrRight_apply
+ piCongrRight_symm_apply
+ refl_apply
+ signSet
+ symm_neg
+ volume_preserving_negAt
- instance : IsAddHaarMeasure (volume : Measure (mixedSpace K)) := prod.instIsAddHaarMeasure _ _

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Ruben-VandeVelde]

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

[jcommelin]

bors d+

[mathlib-bors]

✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

LGTM, thanks!

[riccardobrasca]

There is a merge conflict but otherwise I think it is ready to go.

[riccardobrasca]

Thanks!

bors merge