Documentation Verification Report

NumberField

📁 Source: Mathlib/NumberTheory/Height/NumberField.lean

Statistics

Metric	Count
Definitions `NumberField`, `instAdmissibleAbsValues`, `multisetInfinitePlace`	3
Theorems `count_multisetInfinitePlace_eq_mult`, `mem_multisetInfinitePlace`, `mulHeight_eq`, `mulHeight₁_eq`, `prod_archAbsVal_eq`, `prod_nonarchAbsVal_eq`	6
Total	9

NumberField

Definitions

Name	Category	Theorems
`instAdmissibleAbsValues` 📖	CompOp	4 math math: `prod_nonarchAbsVal_eq`, `mulHeight_eq`, `prod_archAbsVal_eq`, `mulHeight₁_eq`
`multisetInfinitePlace` 📖	CompOp	2 math math: `count_multisetInfinitePlace_eq_mult`, `mem_multisetInfinitePlace`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`count_multisetInfinitePlace_eq_mult` 📖	mathematical	—	`Multiset.count` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `place` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `Complex.instNontrivial` `multisetInfinitePlace` `InfinitePlace.mult`	—	`Complex.instNontrivial` `Multiset.count_bind` `Multiset.map_congr` `Multiset.count_replicate` `Fintype.sum_ite_eq'`
`mem_multisetInfinitePlace` 📖	mathematical	—	`AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Multiset` `Multiset.instMembership` `multisetInfinitePlace` `IsInfinitePlace`	—	`Complex.instNontrivial`
`mulHeight_eq` 📖	mathematical	—	`Height.mulHeight` `instAdmissibleAbsValues` `Real` `Real.instMul` `Finset.prod` `InfinitePlace` `Real.instCommMonoid` `Finset.univ` `InfinitePlace.NumberField.InfinitePlace.fintype` `Monoid.toNatPow` `Real.instMonoid` `iSup` `Real.instSupSet` `DFunLike.coe` `InfinitePlace.instFunLikeReal` `InfinitePlace.mult` `finprod` `FinitePlace` `FinitePlace.instFunLikeReal`	—	`Complex.instNontrivial` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instIsFractionRing` `Height.mulHeight_eq` `prod_archAbsVal_eq` `Finset.prod_congr`
`mulHeight₁_eq` 📖	mathematical	—	`Height.mulHeight₁` `instAdmissibleAbsValues` `Real` `Real.instMul` `Finset.prod` `InfinitePlace` `Real.instCommMonoid` `Finset.univ` `InfinitePlace.NumberField.InfinitePlace.fintype` `Monoid.toNatPow` `Real.instMonoid` `Real.instMax` `DFunLike.coe` `InfinitePlace.instFunLikeReal` `Real.instOne` `InfinitePlace.mult` `finprod` `FinitePlace` `FinitePlace.instFunLikeReal`	—	`Complex.instNontrivial` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instIsFractionRing` `prod_archAbsVal_eq` `Finset.prod_congr`
`prod_archAbsVal_eq` 📖	mathematical	—	`Multiset.prod` `Multiset.map` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Height.AdmissibleAbsValues.archAbsVal` `instAdmissibleAbsValues` `Finset.prod` `InfinitePlace` `Finset.univ` `InfinitePlace.NumberField.InfinitePlace.fintype` `Monoid.toNatPow` `CommMonoid.toMonoid` `RingHom` `Complex` `Semiring.toNonAssocSemiring` `Complex.instSemiring` `place` `NormedField.toNormedDivisionRing` `Complex.instNormedField` `Complex.instNontrivial` `InfinitePlace.mult`	—	—
`prod_nonarchAbsVal_eq` 📖	mathematical	—	`finprod` `Set.Elem` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Height.AdmissibleAbsValues.nonarchAbsVal` `instAdmissibleAbsValues` `Set` `Set.instMembership` `FinitePlace` `IsDedekindDomain.HeightOneSpectrum` `RingOfIntegers` `RingOfIntegers.instCommRing` `WithVal` `WithZero` `Multiplicative` `WithZero.instLinearOrderedCommGroupWithZero` `Multiplicative.commGroup` `Int.instAddCommGroup` `Multiplicative.linearOrder` `Int.instLinearOrder` `DivisionRing.toRing` `Field.toDivisionRing` `IsDedekindDomain.HeightOneSpectrum.valuation` `RingOfIntegers.instIsDedekindDomain` `RingOfIntegers.instAlgebra_1` `Algebra.id` `Semifield.toCommSemiring` `RingOfIntegers.instIsFractionRing` `WithVal.instField` `place` `IsDedekindDomain.HeightOneSpectrum.adicCompletion` `NormedField.toNormedDivisionRing` `instNormedFieldValuedAdicCompletion` `FinitePlace.embedding`	—	—

(root)

Definitions

Name	Category	Theorems
`NumberField` 📖	CompData	9 math math: `AdjoinRoot.instNumberFieldRat`, `CyclotomicField.instNumberField`, `IsCyclotomicExtension.numberField`, `NumberField.of_subfield`, `NumberField.of_tower`, `Rat.numberField`, `NumberField.of_ringEquiv`, `NumberField.of_intermediateField`, `NumberField.of_module_finite`

---

← Back to Index