Commit 2023-06-22 20:54 766fb108

View on Github →

feat: port NumberTheory.NumberField.Embeddings (#5367)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.ComplexEmbedding.IsReal.coe_embedding_apply

added def NumberField.ComplexEmbedding.IsReal.embedding

added theorem NumberField.ComplexEmbedding.IsReal.place_embedding

added def NumberField.ComplexEmbedding.IsReal

added def NumberField.ComplexEmbedding.conjugate

added theorem NumberField.ComplexEmbedding.conjugate_coe_eq

added theorem NumberField.ComplexEmbedding.isReal_conjugate_iff

added theorem NumberField.ComplexEmbedding.isReal_iff

added theorem NumberField.ComplexEmbedding.place_conjugate

added theorem NumberField.ComplexEmbeddings.IsReal.embedding_mk

added theorem NumberField.Embeddings.card

added theorem NumberField.Embeddings.coeff_bdd_of_norm_le

added theorem NumberField.Embeddings.finite_of_norm_le

added theorem NumberField.Embeddings.pow_eq_one_of_norm_eq_one

added theorem NumberField.Embeddings.range_eval_eq_rootSet_minpoly

added def NumberField.InfinitePlace.IsComplex

added theorem NumberField.InfinitePlace.IsReal.abs_embedding_apply

added theorem NumberField.InfinitePlace.IsReal.place_embedding_apply

added def NumberField.InfinitePlace.IsReal

added theorem NumberField.InfinitePlace.abs_embedding

added theorem NumberField.InfinitePlace.apply

added theorem NumberField.InfinitePlace.card_complex_embeddings

added theorem NumberField.InfinitePlace.card_real_embeddings

added theorem NumberField.InfinitePlace.coe_mk

added theorem NumberField.InfinitePlace.eq_iff_eq

added theorem NumberField.InfinitePlace.ext

added theorem NumberField.InfinitePlace.isComplex_iff

added theorem NumberField.InfinitePlace.isReal_iff

added theorem NumberField.InfinitePlace.isReal_or_isComplex

added theorem NumberField.InfinitePlace.le_iff_le

added theorem NumberField.InfinitePlace.mkComplex.apply

added theorem NumberField.InfinitePlace.mkComplex.filter

added theorem NumberField.InfinitePlace.mkComplex.filter_card

added theorem NumberField.InfinitePlace.mkComplex_coe

added theorem NumberField.InfinitePlace.mkComplex_embedding

added theorem NumberField.InfinitePlace.mkReal.apply

added theorem NumberField.InfinitePlace.mkReal_coe

added theorem NumberField.InfinitePlace.mk_conjugate_eq

added theorem NumberField.InfinitePlace.mk_embedding

added theorem NumberField.InfinitePlace.mk_eq_iff

added theorem NumberField.InfinitePlace.not_isComplex_iff_isReal

added theorem NumberField.InfinitePlace.not_isReal_iff_isComplex

added theorem NumberField.InfinitePlace.pos_iff

added theorem NumberField.InfinitePlace.prod_eq_abs_norm

added def NumberField.InfinitePlace

added def NumberField.place

added theorem NumberField.place_apply