Theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq

Modification history

2025-05-05 07:39
Mathlib/NumberTheory/NumberField/Embeddings.lean
chore(NumberField): split `embeddings.lean` (#24478) …
Modified NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eqView on Github →
2024-08-08 10:31
Mathlib/NumberTheory/NumberField/Embeddings.lean
chore: backports for leanprover/lean4#4814 (part 36) (#15612)
Modified NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eqView on Github →
2023-12-26 07:02
Mathlib/NumberTheory/NumberField/Embeddings.lean
feat: The galois group acts on infinite places. (#9280)
Added NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eqView on Github →