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