Commit 2023-08-03 09:17 1bc5bc23

View on Github →

refactor of NumberTheory.NumberField.Embeddings (#6164) Remove unnecessary or redundant results and golf some proofs.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding.lean

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

deleted theorem NumberField.ComplexEmbedding.IsReal.place_embedding

modified def NumberField.ComplexEmbedding.IsReal

modified def NumberField.ComplexEmbedding.conjugate

deleted theorem NumberField.ComplexEmbeddings.IsReal.embedding_mk

modified def NumberField.InfinitePlace.IsComplex

deleted theorem NumberField.InfinitePlace.IsReal.abs_embedding_apply

deleted theorem NumberField.InfinitePlace.IsReal.place_embedding_apply

modified def NumberField.InfinitePlace.IsReal

deleted theorem NumberField.InfinitePlace.abs_embedding

added theorem NumberField.InfinitePlace.card_add_two_mul_card_eq_rank

added theorem NumberField.InfinitePlace.card_filter_mk_eq

deleted theorem NumberField.InfinitePlace.coe_mk

added theorem NumberField.InfinitePlace.embedding_mk_eq

added theorem NumberField.InfinitePlace.embedding_mk_eq_of_isReal

added theorem NumberField.InfinitePlace.embedding_of_isReal_apply

deleted theorem NumberField.InfinitePlace.ext

modified theorem NumberField.InfinitePlace.isReal_iff

added theorem NumberField.InfinitePlace.isReal_of_mk_isReal

deleted theorem NumberField.InfinitePlace.mkComplex.apply

deleted theorem NumberField.InfinitePlace.mkComplex.filter

deleted theorem NumberField.InfinitePlace.mkComplex.filter_card

deleted theorem NumberField.InfinitePlace.mkComplex_embedding

deleted theorem NumberField.InfinitePlace.mkReal.apply

modified theorem NumberField.InfinitePlace.mk_embedding

added theorem NumberField.InfinitePlace.norm_embedding_eq

deleted theorem NumberField.InfinitePlace.not_isComplex_iff_isReal

added theorem NumberField.InfinitePlace.not_isReal_of_mk_isComplex

modified theorem NumberField.InfinitePlace.pos_iff

modified def NumberField.InfinitePlace