Theorems · Definition · number theory

NumberField.FinitePlace.equivHeightOneSpectrum

{K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.FinitePlace K ≃ IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)

The equivalence between finite places and maximal ideals.

Defined in: Mathlib.NumberTheory.NumberField.Completion.FinitePlace
Cited by: 7 results in Mathlib
Foundations: Depth 193 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field NumberField

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites10

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Equivstatement · cited by 8,337
Fieldstatement and proof · cited by 7,404
NumberFieldstatement and proof · cited by 653
NumberField.RingOfIntegersstatement · cited by 413
IsDedekindDomain.HeightOneSpectrumstatement · cited by 338
NumberField.FinitePlacestatement · cited by 35
NumberField.FinitePlace.maximalIdealproof · cited by 10
NumberField.FinitePlace.mkproof · cited by 4
NumberField.FinitePlace.mk_maximalIdealproof · cited by 2
NumberField.FinitePlace.maximalIdeal_mkproof · cited by 0

Cited by7

Results whose statement or proof uses this declaration.

NumberField.FinitePlace.maximalIdeal_injectiveproof · cited by 2
NumberField.FinitePlace.equivHeightOneSpectrum_applystatement and proof · cited by 1
NumberField.FinitePlace.equivHeightOneSpectrum_symm_applystatement · cited by 1
NumberField.FinitePlace.prod_eq_inv_abs_norm_intproof · cited by 1
NumberField.FinitePlace.finprod_finitePlace_pow_multiplicityproof · cited by 0
NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_applystatement · cited by 0
NumberField.FinitePlace.maximalIdeal_injproof · cited by 0