Commit 2024-10-28 15:32 3195aa05

View on Github →

feat(NumberField/CanonicalEmbedding): define the negAt map (#18234) 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.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

added def NumberField.mixedEmbedding.negAt

added theorem NumberField.mixedEmbedding.negAt_apply_abs_of_isReal

added theorem NumberField.mixedEmbedding.negAt_apply_of_isComplex

added theorem NumberField.mixedEmbedding.negAt_apply_of_isReal_and_mem

added theorem NumberField.mixedEmbedding.negAt_apply_of_isReal_and_not_mem

added theorem NumberField.mixedEmbedding.negAt_apply_snd

added theorem NumberField.mixedEmbedding.negAt_signSet_apply_of_isComplex

added theorem NumberField.mixedEmbedding.negAt_signSet_apply_of_isReal

added theorem NumberField.mixedEmbedding.negAt_symm

added theorem NumberField.mixedEmbedding.normAtPlace_negAt

added theorem NumberField.mixedEmbedding.norm_negAt

added def NumberField.mixedEmbedding.signSet

added theorem NumberField.mixedEmbedding.volume_preserving_negAt

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

added theorem ContinuousLinearEquiv.coe_neg

added def ContinuousLinearEquiv.neg

added theorem ContinuousLinearEquiv.neg_apply

added def ContinuousLinearEquiv.piCongrRight

added theorem ContinuousLinearEquiv.piCongrRight_apply

added theorem ContinuousLinearEquiv.piCongrRight_symm_apply

added theorem ContinuousLinearEquiv.refl_apply

added theorem ContinuousLinearEquiv.symm_neg