Theorem NumberField.mixedEmbedding.negAt_signSet_apply_of_isReal

Modification history

2025-02-28 20:41
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
chore(NumberField/CanonicalEmbedding): Fix naming (#21629) …
Deleted NumberField.mixedEmbedding.negAt_signSet_apply_of_isRealView on Github →
2024-10-28 15:32
Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
feat(NumberField/CanonicalEmbedding): define the `negAt` map (#18234) …
Added NumberField.mixedEmbedding.negAt_signSet_apply_of_isRealView on Github →