Commit 2023-12-26 07:02 4fda6f75

View on Github →

feat: The galois group acts on infinite places. (#9280)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.ComplexEmbedding.IsReal.comp

added theorem NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq

added theorem NumberField.ComplexEmbedding.isReal_comp_iff

added theorem NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq

added theorem NumberField.InfinitePlace.IsReal.comap

added def NumberField.InfinitePlace.comap

added theorem NumberField.InfinitePlace.comap_comp

added theorem NumberField.InfinitePlace.comap_mk

added theorem NumberField.InfinitePlace.comap_smul

added theorem NumberField.InfinitePlace.comap_surjective

added theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq

added theorem NumberField.InfinitePlace.isComplex_mk_iff

added theorem NumberField.InfinitePlace.isComplex_smul_iff

added theorem NumberField.InfinitePlace.isReal_comap_iff

added theorem NumberField.InfinitePlace.isReal_mk_iff

added theorem NumberField.InfinitePlace.isReal_smul_iff

added theorem NumberField.InfinitePlace.mem_orbit_iff

added def NumberField.InfinitePlace.orbitRelEquiv

added theorem NumberField.InfinitePlace.orbitRelEquiv_apply_mk''

added theorem NumberField.InfinitePlace.smul_apply

added theorem NumberField.InfinitePlace.smul_eq_comap

added theorem NumberField.InfinitePlace.smul_mk