NumberField

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

Statistics

Metric	Count
Definitions evalHeightTotalWeight, NumberField, instAdmissibleAbsValues, multisetInfinitePlace	4
Theorems count_multisetInfinitePlace_eq_mult, logHeight₁_eq, mem_multisetInfinitePlace, mulHeight_eq, mulHeight₁_eq, prod_archAbsVal_eq, prod_nonarchAbsVal_eq, sum_archAbsVal_eq, sum_nonarchAbsVal_eq, totalWeight_eq_finrank, totalWeight_eq_sum_mult, totalWeight_pos	12
Total	16

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
evalHeightTotalWeight 📖	CompOp	—

NumberField

Definitions

Name	Category	Theorems
instAdmissibleAbsValues 📖	CompOp	10 math math: prod_nonarchAbsVal_eq, mulHeight_eq, totalWeight_eq_sum_mult, sum_nonarchAbsVal_eq, logHeight₁_eq, totalWeight_pos, prod_archAbsVal_eq, totalWeight_eq_finrank, mulHeight₁_eq, sum_archAbsVal_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'
logHeight₁_eq 📖	mathematical	—	Height.logHeight₁ instAdmissibleAbsValues Real Real.instAdd Finset.sum InfinitePlace Real.instAddCommMonoid Finset.univ InfinitePlace.NumberField.InfinitePlace.fintype Real.instMul Real.instNatCast InfinitePlace.mult Real.posLog DFunLike.coe InfinitePlace.instFunLikeReal finsum FinitePlace FinitePlace.instFunLikeReal	—	Complex.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instIsFractionRing RingOfIntegers.instFreeInt Height.logHeight₁_eq sum_archAbsVal_eq Finset.sum_congr
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.toPow Real.instMonoid iSup Real.instSupSet DFunLike.coe InfinitePlace.instFunLikeReal InfinitePlace.mult finprod FinitePlace FinitePlace.instFunLikeReal	—	Complex.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instIsFractionRing RingOfIntegers.instFreeInt 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.toPow Real.instMonoid Real.instMax DFunLike.coe InfinitePlace.instFunLikeReal Real.instOne InfinitePlace.mult finprod FinitePlace FinitePlace.instFunLikeReal	—	Complex.instNontrivial RingOfIntegers.instIsDedekindDomain RingOfIntegers.instIsFractionRing RingOfIntegers.instFreeInt 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.toPow 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 instCommRingRingOfIntegers place IsDedekindDomain.HeightOneSpectrum.adicCompletion RingOfIntegers.instIsDedekindDomain RingOfIntegers.instAlgebra_1 RingOfIntegers.instIsFractionRing NormedField.toNormedDivisionRing HeightOneSpectrum.instNormedFieldValuedAdicCompletion RingOfIntegers.instFreeInt FinitePlace.embedding	—	—
sum_archAbsVal_eq 📖	mathematical	—	Multiset.sum Multiset.map AbsoluteValue Real DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Real.semiring Real.partialOrder Height.AdmissibleAbsValues.archAbsVal instAdmissibleAbsValues Finset.sum InfinitePlace Finset.univ InfinitePlace.NumberField.InfinitePlace.fintype AddMonoid.toNSMul AddCommMonoid.toAddMonoid InfinitePlace.mult RingHom Complex Semiring.toNonAssocSemiring Complex.instSemiring place NormedField.toNormedDivisionRing Complex.instNormedField Complex.instNontrivial	—	Complex.instNontrivial Finset.sum_multiset_map_count Finset.sum_bij' mem_multisetInfinitePlace Multiset.mem_dedup count_multisetInfinitePlace_eq_mult
sum_nonarchAbsVal_eq 📖	mathematical	—	finsum 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 instCommRingRingOfIntegers place IsDedekindDomain.HeightOneSpectrum.adicCompletion RingOfIntegers.instIsDedekindDomain RingOfIntegers.instAlgebra_1 RingOfIntegers.instIsFractionRing NormedField.toNormedDivisionRing HeightOneSpectrum.instNormedFieldValuedAdicCompletion RingOfIntegers.instFreeInt FinitePlace.embedding	—	—
totalWeight_eq_finrank 📖	mathematical	—	Height.totalWeight instAdmissibleAbsValues Module.finrank Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule Rat.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DivisionRing.toRatAlgebra Field.toDivisionRing to_charZero	—	to_charZero totalWeight_eq_sum_mult InfinitePlace.sum_mult_eq
totalWeight_eq_sum_mult 📖	mathematical	—	Height.totalWeight instAdmissibleAbsValues Finset.sum InfinitePlace Nat.instAddCommMonoid Finset.univ InfinitePlace.NumberField.InfinitePlace.fintype InfinitePlace.mult	—	Multiset.sum_map_toList Fin.sum_univ_fun_getElem Multiset.length_toList Fin.sum_const smul_eq_mul mul_one Finset.sum_congr sum_archAbsVal_eq
totalWeight_pos 📖	mathematical	—	Height.totalWeight instAdmissibleAbsValues	—	instNonemptyInfinitePlaceOfRingHomComplex Embeddings.instNonemptyRingHom Complex.instCharZero Complex.isAlgClosed Complex.instNontrivial Multiset.card_bind Multiset.map_congr Multiset.card_replicate Fintype.sum_pos Nat.instIsOrderedCancelAddMonoid Ne.pos Pi.instCanonicallyOrderedAddForall Nat.instCanonicallyOrderedAdd Function.ne_iff InfinitePlace.mult_ne_zero

(root)

Definitions

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

---

← Back to Index