Theorems · Definition · number theory
NumberField.FinitePlace
(K : Type u_3) → [inst : Field K] → [NumberField K] → Type (max 0 u_3)
A finite place of a number field K is a place associated to an embedding into a completion
with respect to a maximal ideal.
- Cited by
- 35 results in Mathlib
- Foundations
- Depth 188 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- FieldNumberField
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realproof · cited by 25,697
- Fieldstatement and proof · cited by 7,404
- NumberFieldstatement and proof · cited by 653
- NumberField.RingOfIntegersproof · cited by 413
- AbsoluteValueproof · cited by 363
- IsDedekindDomain.HeightOneSpectrumproof · cited by 338
- NumberField.placeproof · cited by 71
- NumberField.FinitePlace.embeddingproof · cited by 24
Cited by38
Results whose statement or proof uses this declaration.
- NumberField.FinitePlace.maximalIdealstatement and proof · cited by 10
- NumberField.FinitePlace.equivHeightOneSpectrumstatement · cited by 7
- NumberField.FinitePlace.mkstatement · cited by 4
- NumberField.mulHeight_eqstatement and proof · cited by 3
- NumberField.FinitePlace.hasFiniteMulSupport_intstatement and proof · cited by 3
- Rat.mulHeight_eq_max_abs_of_gcd_eq_oneproof · cited by 2
- NumberField.FinitePlace.maximalIdeal_injectivestatement · cited by 2
- NumberField.FinitePlace.mk_maximalIdealstatement and proof · cited by 2
- NumberField.FinitePlace.norm_embedding_eqstatement and proof · cited by 2
- NumberField.FinitePlace.add_lestatement and proof · cited by 1
- NumberField.absNorm_mul_finprod_finitePlace_eq_onestatement and proof · cited by 1
- NumberField.FinitePlace.equivHeightOneSpectrum_applystatement and proof · cited by 1