Mathlib Changelog
v4
Changelog
About
Github
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