Structures · Algebra
NumberField
A number field is a field which has characteristic zero and is finite dimensional over ℚ.
- Defined in
- Mathlib.NumberTheory.NumberField.Basic
- Shape
- One type argument · adds to_charZero, to_finiteDimensional
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances5
- Rat
- WithVal
- AdjoinRoot
- CyclotomicField
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by786
- NumberField.Units.dirichletUnitTheorem.w₀
- NumberField.discr
- NumberField.InfinitePlace.nrComplexPlaces
- NumberField.mixedEmbedding.norm
- NumberField.Units.dirichletUnitTheorem.logSpace
- NumberField.Units.rank
- NumberField.FinitePlace
- NumberField.InfinitePlace.nrRealPlaces
- NumberField.mixedEmbedding.fundamentalCone.expMapBasis
- NumberField.integralBasis
- NumberField.Units.logEmbedding
- NumberField.mixedEmbedding.fundamentalCone.expMap
- NumberField.Units.fundSystem
- NumberField.mixedEmbedding.fundamentalCone
- NumberField.mixedEmbedding.fundamentalCone.integerSet
- NumberField.mixedEmbedding.minkowskiBound
- NumberField.Units.unitLattice
- NumberField.mixedEmbedding.logMap
- NumberField.Units.regulator
- IsCyclotomicExtension.numberField
- NumberField.mixedEmbedding.fundamentalCone.paramSet
- NumberField.Units.basisUnitLattice
- NumberField.mixedEmbedding.fundamentalCone.completeBasis
- NumberField.mixedEmbedding.polarCoord
- NumberField.house
- NumberField.mixedEmbedding.fundamentalCone.normLeOne
- NumberField.mixedEmbedding.fundamentalCone.preimageOfMemIntegerSet
- NumberField.mixedEmbedding.convexBodySumFun
- NumberField.mixedEmbedding.polarCoordReal
- NumberField.mixedEmbedding.convexBodyLTFactor
- NumberField.RingOfIntegers.basis
- NumberField.Units.IsMaxRank
- NumberField.Units.regOfFamily
- IsCyclotomicExtension.Rat.galEquivZMod
- NumberField.mixedEmbedding.fractionalIdealLatticeBasis
- NumberField.mixedEmbedding.convexBodySum
- NumberField.mixedEmbedding.fundamentalCone.compactSet
- NumberField.mixedEmbedding.polarSpaceCoord
- NumberField.mixedEmbedding.latticeBasis
- NumberField.FinitePlace.maximalIdeal
- NumberField.mixedEmbedding.fundamentalCone.equivFinRank
- NumberField.mixedEmbedding.stdBasis
- NumberField.Ideal.primesOverSpanEquivMonicFactorsMod
- NumberField.Units.basisOfIsMaxRank
- NumberField.basisMatrix
- NumberField.IsCMField.unitsMulComplexConjInv
- NumberField.InfinitePlace.card_add_two_mul_card_eq_rank
- NumberField.Set.HasDirichletDensity
- NumberField.basisOfFractionalIdeal
- NumberField.mixedEmbedding.fundamentalCone.idealSet
Ancestors0
No ancestors.