Basic

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

Statistics

Metric	Count
Definitions `logHeight`, `mulHeight`, `AdmissibleAbsValues`, `archAbsVal`, `nonarchAbsVal`, `logHeight`, `logHeight₁`, `mulHeight`, `mulHeight₁`, `totalWeight`, `evalLogHeight`, `evalLogHeight₁`, `evalMulHeight`, `evalMulHeight₁`	14
Theorems `max_abv_sum_one_le`, `max_abv_sum_one_le_of_isNonarchimedean`, `logHeight_eq_log_mulHeight`, `isNonarchimedean`, `mulSupport_finite`, `product_formula`, `fun_logHeight_one`, `fun_logHeight_zero`, `fun_mulHeight_one`, `fun_mulHeight_zero`, `logHeight_eq_log_mulHeight`, `logHeight_nonneg`, `logHeight_one`, `logHeight_pow`, `logHeight_smul_eq_logHeight`, `logHeight_zero`, `logHeight₁_add_le`, `logHeight₁_div_eq_logHeight`, `logHeight₁_eq_logHeight`, `logHeight₁_eq_log_mulHeight₁`, `logHeight₁_inv`, `logHeight₁_neg`, `logHeight₁_one`, `logHeight₁_pow`, `logHeight₁_sub_le`, `logHeight₁_sum_le`, `logHeight₁_zero`, `logHeight₁_zpow`, `mulHeight_comp_equiv`, `mulHeight_eq`, `mulHeight_ne_zero`, `mulHeight_one`, `mulHeight_pos`, `mulHeight_pow`, `mulHeight_smul_eq_mulHeight`, `mulHeight_swap`, `mulHeight_zero`, `mulHeight₁_add_le`, `mulHeight₁_div_eq_mulHeight`, `mulHeight₁_eq`, `mulHeight₁_eq_mulHeight`, `mulHeight₁_inv`, `mulHeight₁_ne_zero`, `mulHeight₁_neg`, `mulHeight₁_nonneg`, `mulHeight₁_one`, `mulHeight₁_pos`, `mulHeight₁_pow`, `mulHeight₁_sub_le`, `mulHeight₁_sum_le`, `mulHeight₁_zero`, `mulHeight₁_zpow`, `one_le_mulHeight`, `one_le_mulHeight₁`, `zero_le_logHeight₁`	55
Total	69

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`max_abv_sum_one_le` 📖	mathematical	`Nonempty`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `AbsoluteValue.funLike` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `AddMonoidWithOne.toNatCast` `card` `prod` `CommSemiring.toCommMonoid`	—	`sup_le` `nsmul_eq_mul` `sum_const` `le_imp_le_of_le_of_le` `AbsoluteValue.sum_le` `le_refl` `sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `le_prod_max_one` `IsOrderedRing.toZeroLEOneClass` `IsOrderedRing.toPosMulMono` `mul_one` `mul_le_mul` `IsOrderedRing.toMulPosMono` `one_le_prod` `le_max_right` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `instNontrivialOfCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Nat.cast_nonneg'`
`max_abv_sum_one_le_of_isNonarchimedean` 📖	mathematical	`IsNonarchimedean` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AbsoluteValue` `CommSemiring.toSemiring` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AbsoluteValue.funLike`	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `prod` `CommSemiring.toCommMonoid`	—	`eq_empty_or_nonempty` `AbsoluteValue.map_zero` `sup_of_le_right` `IsOrderedRing.toZeroLEOneClass` `sup_le` `le_imp_le_of_le_of_le` `IsNonarchimedean.apply_sum_le_sup_of_isNonarchimedean` `le_refl` `sup'_le` `le_prod_max_one` `IsOrderedRing.toPosMulMono` `one_le_prod` `le_max_right`

Finsupp

Definitions

Name	Category	Theorems
`logHeight` 📖	CompOp	—
`mulHeight` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`logHeight_eq_log_mulHeight` 📖	mathematical	—	`Height.logHeight` `DFunLike.coe` `Finsupp` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `instFunLike` `Real.log` `Height.mulHeight`	—	—

Height

Definitions

Name	Category	Theorems
`AdmissibleAbsValues` 📖	CompData	—
`logHeight` 📖	CompOp	11 math math: `logHeight₁_div_eq_logHeight`, `logHeight_one`, `logHeight_zero`, `fun_logHeight_zero`, `fun_logHeight_one`, `logHeight_eq_log_mulHeight`, `logHeight_nonneg`, `logHeight₁_eq_logHeight`, `Finsupp.logHeight_eq_log_mulHeight`, `logHeight_smul_eq_logHeight`, `logHeight_pow`
`logHeight₁` 📖	CompOp	13 math math: `logHeight₁_pow`, `logHeight₁_sum_le`, `logHeight₁_add_le`, `logHeight₁_sub_le`, `logHeight₁_neg`, `logHeight₁_one`, `logHeight₁_div_eq_logHeight`, `zero_le_logHeight₁`, `logHeight₁_inv`, `logHeight₁_zpow`, `logHeight₁_eq_logHeight`, `logHeight₁_zero`, `logHeight₁_eq_log_mulHeight₁`
`mulHeight` 📖	CompOp	16 math math: `fun_mulHeight_zero`, `one_le_mulHeight`, `NumberField.mulHeight_eq`, `mulHeight_pow`, `mulHeight_comp_equiv`, `mulHeight_pos`, `mulHeight_swap`, `mulHeight_zero`, `mulHeight_smul_eq_mulHeight`, `mulHeight_eq`, `logHeight_eq_log_mulHeight`, `mulHeight₁_eq_mulHeight`, `fun_mulHeight_one`, `Finsupp.logHeight_eq_log_mulHeight`, `mulHeight₁_div_eq_mulHeight`, `mulHeight_one`
`mulHeight₁` 📖	CompOp	17 math math: `mulHeight₁_eq`, `mulHeight₁_zpow`, `mulHeight₁_pow`, `mulHeight₁_add_le`, `one_le_mulHeight₁`, `mulHeight₁_sum_le`, `mulHeight₁_pos`, `mulHeight₁_sub_le`, `mulHeight₁_inv`, `mulHeight₁_nonneg`, `mulHeight₁_eq_mulHeight`, `mulHeight₁_div_eq_mulHeight`, `mulHeight₁_zero`, `NumberField.mulHeight₁_eq`, `logHeight₁_eq_log_mulHeight₁`, `mulHeight₁_neg`, `mulHeight₁_one`
`totalWeight` 📖	CompOp	6 math math: `logHeight₁_sum_le`, `logHeight₁_add_le`, `logHeight₁_sub_le`, `mulHeight₁_add_le`, `mulHeight₁_sum_le`, `mulHeight₁_sub_le`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fun_logHeight_one` 📖	mathematical	—	`logHeight` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instZero`	—	`logHeight_one`
`fun_logHeight_zero` 📖	mathematical	—	`logHeight` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instZero`	—	`logHeight_zero`
`fun_mulHeight_one` 📖	mathematical	—	`mulHeight` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instOne`	—	`mulHeight_one`
`fun_mulHeight_zero` 📖	mathematical	—	`mulHeight` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instOne`	—	`mulHeight_zero`
`logHeight_eq_log_mulHeight` 📖	mathematical	—	`logHeight` `Real.log` `mulHeight`	—	—
`logHeight_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `logHeight`	—	`Real.log_nonneg` `one_le_mulHeight`
`logHeight_one` 📖	mathematical	—	`logHeight` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instZero`	—	`mulHeight_one` `Real.log_one`
`logHeight_pow` 📖	mathematical	—	`logHeight` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.instMul` `Real.instNatCast`	—	`mulHeight_pow` `Real.log_pow`
`logHeight_smul_eq_logHeight` 📖	mathematical	—	`logHeight` `Function.hasSMul` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id`	—	`mulHeight_smul_eq_mulHeight`
`logHeight_zero` 📖	mathematical	—	`logHeight` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instZero`	—	`mulHeight_zero` `Real.log_one`
`logHeight₁_add_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight₁` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instAdd` `Real.instMul` `Real.instNatCast` `totalWeight` `Real.log` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Meta.NormNum.instAtLeastTwo` `mulHeight₁_pos` `mul_pos` `Real.log_le_log` `mulHeight₁_add_le`
`logHeight₁_div_eq_logHeight` 📖	mathematical	—	`logHeight₁` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `logHeight` `Matrix.vecCons` `Matrix.vecEmpty`	—	`logHeight₁_eq_log_mulHeight₁` `logHeight_eq_log_mulHeight` `mulHeight₁_div_eq_mulHeight`
`logHeight₁_eq_logHeight` 📖	mathematical	—	`logHeight₁` `logHeight` `Matrix.vecCons` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Matrix.vecEmpty`	—	`mulHeight₁_eq_mulHeight`
`logHeight₁_eq_log_mulHeight₁` 📖	mathematical	—	`logHeight₁` `Real.log` `mulHeight₁`	—	—
`logHeight₁_inv` 📖	mathematical	—	`logHeight₁` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`mulHeight₁_inv`
`logHeight₁_neg` 📖	mathematical	—	`logHeight₁` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`mulHeight₁_neg`
`logHeight₁_one` 📖	mathematical	—	`logHeight₁` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instZero`	—	`mulHeight₁_one` `Real.log_one`
`logHeight₁_pow` 📖	mathematical	—	`logHeight₁` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.instMul` `Real.instNatCast`	—	`mulHeight₁_pow` `Real.log_pow`
`logHeight₁_sub_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight₁` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instAdd` `Real.instMul` `Real.instNatCast` `totalWeight` `Real.log` `instOfNatAtLeastTwo` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `logHeight₁_neg` `logHeight₁_add_le`
`logHeight₁_sum_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight₁` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instAdd` `Real.instMul` `Real.instNatCast` `totalWeight` `Real.log` `Finset.card` `Real.instAddCommMonoid`	—	`Finset.eq_empty_or_nonempty` `logHeight₁_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Real.log_zero` `MulZeroClass.mul_zero` `add_zero` `Finset.sum_congr` `ne_of_gt` `mulHeight₁_pos` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `Finset.Nonempty.ne_empty` `Finset.prod_pos` `Real.instZeroLEOneClass` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.log_le_log` `mulHeight₁_sum_le`
`logHeight₁_zero` 📖	mathematical	—	`logHeight₁` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instZero`	—	`mulHeight₁_zero` `Real.log_one`
`logHeight₁_zpow` 📖	mathematical	—	`logHeight₁` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Real` `Real.instMul` `Real.instNatCast`	—	`mulHeight₁_zpow` `Real.log_pow`
`mulHeight_comp_equiv` 📖	mathematical	—	`mulHeight` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`Equiv.iSup_congr` `eq_or_ne` `mulHeight_zero` `Function.ne_iff` `Equiv.apply_symm_apply` `mulHeight_eq` `Multiset.map_congr`
`mulHeight_eq` 📖	mathematical	—	`mulHeight` `Real` `Real.instMul` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `iSup` `Real.instSupSet` `DFunLike.coe` `AbsoluteValue.funLike` `AdmissibleAbsValues.archAbsVal` `finprod` `Set.Elem` `AdmissibleAbsValues.nonarchAbsVal` `Set` `Set.instMembership`	—	—
`mulHeight_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `mulHeight_pos`
`mulHeight_one` 📖	mathematical	—	`mulHeight` `Pi.instOne` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instOne`	—	`isEmpty_or_nonempty` `Unique.instSubsingleton` `mulHeight_zero` `NeZero.one` `Function.nontrivial` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mulHeight_eq` `Multiset.map_congr` `AbsoluteValue.map_one` `Real.instIsDomain` `ciSup_const` `Multiset.map_const'` `Multiset.prod_replicate` `one_pow` `finprod_one` `mul_one`
`mulHeight_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `mulHeight`	—	`LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_le_mulHeight`
`mulHeight_pow` 📖	mathematical	—	`mulHeight` `Pi.instPow` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.instMonoid`	—	`eq_or_ne` `pow_zero` `mulHeight_one` `mulHeight_zero` `zero_pow` `one_pow` `Function.ne_iff` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Real.coe_toNNReal` `AbsoluteValue.nonneg` `Monotone.map_ciSup_of_continuousAt` `NNReal.instOrderTopology` `OrderTopology.to_orderClosedTopology` `Continuous.continuousAt` `continuous_pow` `IsTopologicalSemiring.toContinuousMul` `NNReal.instIsTopologicalSemiring` `pow_left_mono` `NNReal.mulLeftMono` `covariant_swap_mul_of_covariant_mul` `Finite.bddAbove_range` `instIsDirectedOrder` `NNReal.instIsOrderedRing` `NNReal.instArchimedean` `instIsReducedForall` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `Function.nontrivial` `mulHeight_eq` `Multiset.map_congr` `mul_pow` `finprod_pow`
`mulHeight_smul_eq_mulHeight` 📖	mathematical	—	`mulHeight` `Function.hasSMul` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `Algebra.id`	—	`eq_or_ne` `smul_zero` `Function.ne_iff` `mulHeight_eq` `Multiset.map_congr` `map_mul` `AbsoluteValue.mulHomClass` `Real.mul_iSup_of_nonneg` `AbsoluteValue.nonneg` `Multiset.prod_map_mul` `finprod_mul_distrib` `AdmissibleAbsValues.mulSupport_finite` `mul_mul_mul_comm` `AdmissibleAbsValues.product_formula` `one_mul`
`mulHeight_swap` 📖	mathematical	—	`mulHeight` `Matrix.vecCons` `Matrix.vecEmpty`	—	`mulHeight_comp_equiv`
`mulHeight_zero` 📖	mathematical	—	`mulHeight` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instOne`	—	—
`mulHeight₁_add_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight₁` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `totalWeight`	—	`Nat.instAtLeastTwoHAddOfNat` `Finset.sum_congr` `Fin.sum_univ_two` `Matrix.cons_val_fin_one` `mul_assoc` `le_imp_le_of_le_of_le` `mulHeight₁_sum_le` `Finset.univ_nonempty` `le_refl` `Fintype.card_fin` `Finset.prod_congr` `Fin.prod_univ_two`
`mulHeight₁_div_eq_mulHeight` 📖	mathematical	—	`mulHeight₁` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `mulHeight` `Matrix.vecCons` `Matrix.vecEmpty`	—	`eq_or_ne` `div_zero` `mulHeight₁_zero` `Matrix.zero_empty` `mulHeight_zero` `mulHeight_smul_eq_mulHeight` `Finite.of_fintype` `Matrix.smul_cons` `mul_one` `MulZeroClass.mul_zero` `Matrix.smul_empty` `mulHeight_swap` `mulHeight₁_eq_mulHeight` `mul_div_cancel₀`
`mulHeight₁_eq` 📖	mathematical	—	`mulHeight₁` `Real` `Real.instMul` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Real.instMax` `DFunLike.coe` `AbsoluteValue.funLike` `Real.instOne` `AdmissibleAbsValues.archAbsVal` `finprod` `Set.Elem` `AdmissibleAbsValues.nonarchAbsVal` `Set` `Set.instMembership`	—	—
`mulHeight₁_eq_mulHeight` 📖	mathematical	—	`mulHeight₁` `mulHeight` `Matrix.vecCons` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Matrix.vecEmpty`	—	`Fintype.complete` `Matrix.cons_val_fin_one` `AbsoluteValue.map_one` `Real.instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `NeZero.one` `Matrix.zero_empty` `Multiset.map_congr` `mulHeight_eq`
`mulHeight₁_inv` 📖	mathematical	—	`mulHeight₁` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield`	—	`mulHeight₁_eq_mulHeight` `eq_or_ne` `inv_zero` `Fintype.complete` `mul_inv_cancel₀` `Matrix.cons_val_fin_one` `mul_one` `mulHeight_smul_eq_mulHeight` `Finite.of_fintype` `mulHeight_swap`
`mulHeight₁_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `mulHeight₁_pos`
`mulHeight₁_neg` 📖	mathematical	—	`mulHeight₁` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`Multiset.map_congr` `AddGroupSeminormClass.map_neg_eq_map` `MulRingSeminormClass.toAddGroupSeminormClass` `MulRingNormClass.toMulRingSeminormClass` `AbsoluteValue.instMulRingNormClassOfNontrivialOfIsDomain` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Real.instIsDomain`
`mulHeight₁_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `mulHeight₁`	—	`LT.lt.le` `mulHeight₁_pos`
`mulHeight₁_one` 📖	mathematical	—	`mulHeight₁` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instOne`	—	`Multiset.map_congr` `AbsoluteValue.map_one` `Real.instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `max_self` `Multiset.map_const'` `Multiset.prod_replicate` `one_pow` `finprod_one` `mul_one`
`mulHeight₁_pos` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `mulHeight₁`	—	`LT.lt.trans_le` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `one_le_mulHeight₁`
`mulHeight₁_pow` 📖	mathematical	—	`mulHeight₁` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.instMonoid`	—	`mulHeight₁_eq_mulHeight` `mulHeight_pow` `Finite.of_fintype` `Fintype.complete` `Matrix.cons_val_fin_one` `one_pow`
`mulHeight₁_sub_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight₁` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `instOfNatAtLeastTwo` `Real.instNatCast` `Nat.instAtLeastTwoHAddOfNat` `totalWeight`	—	`Nat.instAtLeastTwoHAddOfNat` `sub_eq_add_neg` `mulHeight₁_neg` `mulHeight₁_add_le`
`mulHeight₁_sum_le` 📖	mathematical	`Finset.Nonempty`	`Real` `Real.instLE` `mulHeight₁` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instMul` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Finset.card` `totalWeight` `Finset.prod` `Real.instCommMonoid`	—	`Finset.prod_congr` `Finset.prod_mul_distrib` `Multiset.prod_replicate` `Multiset.map_const` `finprod_prod_comm` `Multiset.prod_map_prod` `mul_assoc` `Multiset.prod_map_mul` `Multiset.map_congr` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Multiset.prod_map_le_prod_map₀` `Real.instZeroLEOneClass` `le_of_lt` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Finset.max_abv_sum_one_le` `RCLike.charZero_rclike` `finprod_le_finprod` `Set.Finite.subset` `Set.Finite.biUnion` `Finset.finite_toSet` `Finset.mulSupport_prod` `Finset.max_abv_sum_one_le_of_isNonarchimedean` `AdmissibleAbsValues.isNonarchimedean` `Subtype.prop` `finprod_nonneg` `Multiset.prod_map_nonneg` `mul_nonneg` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finset.prod_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing`
`mulHeight₁_zero` 📖	mathematical	—	`mulHeight₁` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instOne`	—	`Multiset.map_congr` `AbsoluteValue.map_zero` `sup_of_le_right` `Real.instZeroLEOneClass` `Multiset.map_const'` `Multiset.prod_replicate` `one_pow` `finprod_one` `mul_one`
`mulHeight₁_zpow` 📖	mathematical	—	`mulHeight₁` `DivInvMonoid.toZPow` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `Real` `Monoid.toNatPow` `Real.instMonoid`	—	`le_or_gt` `CanLift.prf` `instCanLiftIntNatCastLeOfNat` `zpow_natCast` `mulHeight₁_pow` `zpow_neg` `mulHeight₁_inv`
`one_le_mulHeight` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `mulHeight`	—	`eq_or_ne` `mulHeight_zero` `Function.ne_iff` `mulHeight_smul_eq_mulHeight` `inv_ne_zero` `mulHeight_eq` `one_le_mul_of_one_le_of_one_le` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Multiset.one_le_prod_map` `le_ciSup_of_le` `Finite.bddAbove_range` `instIsDirectedOrder` `Real.instArchimedean` `le_of_eq` `AbsoluteValue.map_mul` `map_inv₀` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `inv_mul_cancel₀` `AbsoluteValue.ne_zero_iff` `one_le_finprod`
`one_le_mulHeight₁` 📖	mathematical	—	`Real` `Real.instLE` `Real.instOne` `mulHeight₁`	—	`one_le_mul_of_one_le_of_one_le` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `Multiset.one_le_prod_map` `le_max_right` `one_le_finprod`
`zero_le_logHeight₁` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `logHeight₁`	—	`Real.log_nonneg` `one_le_mulHeight₁`

Height.AdmissibleAbsValues

Definitions

Name	Category	Theorems
`archAbsVal` 📖	CompOp	4 math math: `Height.mulHeight₁_eq`, `Height.mulHeight_eq`, `NumberField.prod_archAbsVal_eq`, `product_formula`
`nonarchAbsVal` 📖	CompOp	5 math math: `NumberField.prod_nonarchAbsVal_eq`, `Height.mulHeight₁_eq`, `Height.mulHeight_eq`, `mulSupport_finite`, `product_formula`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNonarchimedean` 📖	mathematical	`AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Set` `Set.instMembership` `nonarchAbsVal`	`IsNonarchimedean` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DFunLike.coe` `AbsoluteValue.funLike`	—	—
`mulSupport_finite` 📖	mathematical	—	`Set.Finite` `Set.Elem` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `nonarchAbsVal` `Function.mulSupport` `Real.instOne` `DFunLike.coe` `AbsoluteValue.funLike` `Set` `Set.instMembership`	—	—
`product_formula` 📖	mathematical	—	`Real` `Real.instMul` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `DFunLike.coe` `AbsoluteValue.funLike` `archAbsVal` `finprod` `Set.Elem` `nonarchAbsVal` `Set` `Set.instMembership` `Real.instOne`	—	—

Mathlib.Meta.Positivity

Definitions

Name	Category	Theorems
`evalLogHeight` 📖	CompOp	—
`evalLogHeight₁` 📖	CompOp	—
`evalMulHeight` 📖	CompOp	—
`evalMulHeight₁` 📖	CompOp	—

---

← Back to Index