Commit 2024-12-07 12:21 21d992dd

View on Github →

feat(NumberTheory/NumberField/FinitePlaces): the finite places of a number field (#19667) This file defines finite places of a number field K as absolute values coming from an embedding into a completion of K associated to a non-zero prime ideal of 𝓞 K with some basic APIs. This is part of a project which aims to define heights. The next step is the product formula.

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/FinitePlaces.lean

added theorem NumberField.FinitePlace.apply

added theorem NumberField.FinitePlace.maximalIdeal_inj

added theorem NumberField.FinitePlace.maximalIdeal_injective

added theorem NumberField.FinitePlace.maximalIdeal_mk

added theorem NumberField.FinitePlace.mk_eq_iff

added theorem NumberField.FinitePlace.mk_maximalIdeal

added theorem NumberField.FinitePlace.mulSupport_finite

added theorem NumberField.FinitePlace.mulSupport_finite_int

added theorem NumberField.FinitePlace.norm_def'

added theorem NumberField.FinitePlace.norm_def

added theorem NumberField.FinitePlace.norm_def_int

added theorem NumberField.FinitePlace.norm_embedding_eq

added theorem NumberField.FinitePlace.pos_iff

added def NumberField.FinitePlace

added def NumberField.embedding

added theorem NumberField.norm_eq_one_iff_not_mem

added theorem NumberField.norm_le_one

added theorem NumberField.norm_lt_one_iff_mem

added theorem NumberField.one_lt_norm

added theorem NumberField.toNNReal_Valued_eq_vadicAbv

added theorem NumberField.vadicAbv_def