Commit 2022-12-23 08:51 51c6beb4

View on Github →

feat(number_theory/number_field/embeddings) : add infinite_places (#17844) This PR adds definitions and basic lemmas about places, complex embeddings and infinite places of number field.

Estimated changes

Modified src/algebra/star/basic.lean

modified theorem ring_hom.star_apply

modified theorem ring_hom.star_def

Modified src/analysis/normed/field/basic.lean

Modified src/number_theory/number_field/embeddings.lean

added def number_field.complex_embedding.conjugate

added theorem number_field.complex_embedding.conjugate_coe_eq

added theorem number_field.complex_embedding.is_real.coe_embedding_apply

added def number_field.complex_embedding.is_real.embedding

added theorem number_field.complex_embedding.is_real.place_embedding

added def number_field.complex_embedding.is_real

added theorem number_field.complex_embedding.is_real_conjugate_iff

added theorem number_field.complex_embedding.is_real_iff

added theorem number_field.complex_embedding.place_conjugate

added theorem number_field.infinite_place.apply

added theorem number_field.infinite_place.coe_mk

added theorem number_field.infinite_place.mk_embedding

added theorem number_field.infinite_place.pos_iff

added def number_field.infinite_place

added def number_field.place

added theorem number_field.place_apply

Modified src/topology/algebra/ring.lean

added def absolute_value.comp

Modified src/topology/metric_space/cau_seq_filter.lean