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