Commit 2023-12-26 13:40 5a809b6a

View on Github →

feat: Define IsUnramified for infinite places (#9285)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk

added theorem NumberField.ComplexEmbedding.IsConj.eq

added theorem NumberField.ComplexEmbedding.IsConj.ext

added theorem NumberField.ComplexEmbedding.IsConj.ext_iff

added theorem NumberField.ComplexEmbedding.IsConj.isReal_comp

added theorem NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff

added theorem NumberField.ComplexEmbedding.IsConj.symm

added def NumberField.ComplexEmbedding.IsConj

added theorem NumberField.ComplexEmbedding.isConj_one_iff

added theorem NumberField.ComplexEmbedding.isConj_symm

added theorem NumberField.InfinitePlace.IsReal.isUnramified

added theorem NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot

added def NumberField.InfinitePlace.IsUnramified

added def NumberField.InfinitePlace.IsUnramifiedIn

added theorem NumberField.InfinitePlace.card_eq_card_isUnramifiedIn

added theorem NumberField.InfinitePlace.card_isUnramified

added theorem NumberField.InfinitePlace.card_isUnramified_compl

added theorem NumberField.InfinitePlace.card_stabilizer

added theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramified

added theorem NumberField.InfinitePlace.even_card_aut_of_not_isUnramifiedIn

added theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramified

added theorem NumberField.InfinitePlace.even_finrank_of_not_isUnramifiedIn

added theorem NumberField.InfinitePlace.even_nat_card_aut_of_not_isUnramified

modified theorem NumberField.InfinitePlace.exists_smul_eq_of_comap_eq

added theorem NumberField.InfinitePlace.isUnramifiedIn_comap

added theorem NumberField.InfinitePlace.isUnramified_iff

added theorem NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one

added theorem NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot

added theorem NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj

added theorem NumberField.InfinitePlace.isUnramified_smul_iff

added theorem NumberField.InfinitePlace.mem_stabilizer_mk_iff

added theorem NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two

added theorem NumberField.InfinitePlace.not_isComplex_iff_isReal

added theorem NumberField.InfinitePlace.not_isUnramified_iff

added theorem NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two