Documentation
Mathlib
.
NumberTheory
.
NumberField
.
FinitePlaces
Search
return to top
source
Imports
Init
Mathlib.Algebra.FiniteSupport.Basic
Mathlib.Algebra.GroupWithZero.Range
Mathlib.Data.Int.WithZero
Mathlib.LinearAlgebra.FreeModule.IdealQuotient
Mathlib.RingTheory.DedekindDomain.AdicValuation
Mathlib.RingTheory.DedekindDomain.Factorization
Mathlib.RingTheory.Valuation.Archimedean
Mathlib.Algebra.Order.Archimedean.Submonoid
Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
Mathlib.RingTheory.Ideal.Norm.AbsNorm
Mathlib.RingTheory.Valuation.Discrete.RankOne
Mathlib.Topology.Algebra.Valued.NormedValued
Imported by