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`, `hasFiniteMulSupport`, `isNonarchimedean`, `mulSupport_finite`, `product_formula`, `fun_logHeight_one`, `fun_logHeight_zero`, `fun_mulHeight_one`, `fun_mulHeight_zero`, `logHeight_comp_equiv`, `logHeight_comp_le`, `logHeight_cons_cons_cons_zero`, `logHeight_cons_cons_zero`, `logHeight_cons_zero`, `logHeight_eq_logHeight_restrict_support`, `logHeight_eq_log_mulHeight`, `logHeight_eq_zero_of_subsingleton`, `logHeight_fun_mul_eq`, `logHeight_fun_prod_eq`, `logHeight_mul_le`, `logHeight_neg`, `logHeight_nonneg`, `logHeight_one`, `logHeight_pow`, `logHeight_smul_eq_logHeight`, `logHeight_sumElim_zero_eq`, `logHeight_swap`, `logHeight_zero`, `logHeight₁_add_le`, `logHeight₁_div_eq_logHeight`, `logHeight₁_eq`, `logHeight₁_eq_logHeight`, `logHeight₁_eq_log_mulHeight₁`, `logHeight₁_inv`, `logHeight₁_mul_le`, `logHeight₁_neg`, `logHeight₁_one`, `logHeight₁_pow`, `logHeight₁_prod_le`, `logHeight₁_sub_le`, `logHeight₁_sum_le`, `logHeight₁_zero`, `logHeight₁_zpow`, `mulHeight_comp_equiv`, `mulHeight_comp_le`, `mulHeight_cons_cons_cons_zero`, `mulHeight_cons_cons_zero`, `mulHeight_cons_zero`, `mulHeight_eq`, `mulHeight_eq_mulHeight_restrict_support`, `mulHeight_eq_one_of_subsingleton`, `mulHeight_fun_mul_eq`, `mulHeight_fun_prod_eq`, `mulHeight_mul_le`, `mulHeight_ne_zero`, `mulHeight_neg`, `mulHeight_one`, `mulHeight_pos`, `mulHeight_pow`, `mulHeight_smul_eq_mulHeight`, `mulHeight_sumElim_zero_eq`, `mulHeight_swap`, `mulHeight_zero`, `mulHeight₁_add_le`, `mulHeight₁_div_eq_mulHeight`, `mulHeight₁_eq`, `mulHeight₁_eq_mulHeight`, `mulHeight₁_inv`, `mulHeight₁_mul_le`, `mulHeight₁_ne_zero`, `mulHeight₁_neg`, `mulHeight₁_nonneg`, `mulHeight₁_one`, `mulHeight₁_pos`, `mulHeight₁_pow`, `mulHeight₁_prod_le`, `mulHeight₁_sub_le`, `mulHeight₁_sum_le`, `mulHeight₁_zero`, `mulHeight₁_zpow`, `one_le_mulHeight`, `one_le_mulHeight₁`, `zero_le_logHeight₁`	85
Total	99

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` `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` `prod` `CommSemiring.toCommMonoid`	—	`eq_empty_or_nonempty` `AbsoluteValue.map_zero` `sup_of_le_right` `IsOrderedRing.toZeroLEOneClass` `instReflLe` `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	33 math math: `logHeight_eval_ge`, `logHeight_swap`, `logHeight_sym2_le`, `logHeight_eval_ge'`, `logHeight_cons_cons_cons_zero`, `abs_logHeight_sym2_sub_le`, `logHeight_eval_le'`, `logHeight₁_div_eq_logHeight`, `logHeight_comp_equiv`, `logHeight_one`, `logHeight_zero`, `fun_logHeight_zero`, `logHeight_mul_le`, `fun_logHeight_one`, `logHeight_eq_zero_of_subsingleton`, `logHeight_eq_log_mulHeight`, `logHeight_nonneg`, `logHeight_fun_mul_eq`, `logHeight_neg`, `logHeight_eval_le`, `logHeight₁_eq_logHeight`, `logHeight_linearMap_apply_le`, `Finsupp.logHeight_eq_log_mulHeight`, `logHeight_eq_logHeight_restrict_support`, `logHeight_sym2_ge`, `Projectivization.logHeight_mk`, `logHeight_cons_cons_zero`, `logHeight_smul_eq_logHeight`, `logHeight_fun_prod_eq`, `logHeight_pow`, `logHeight_comp_le`, `logHeight_sumElim_zero_eq`, `logHeight_cons_zero`
`logHeight₁` 📖	CompOp	17 math math: `logHeight₁_pow`, `logHeight₁_sum_le`, `logHeight₁_add_le`, `logHeight₁_sub_le`, `logHeight₁_neg`, `logHeight₁_mul_le`, `logHeight₁_one`, `logHeight₁_div_eq_logHeight`, `logHeight₁_eq`, `zero_le_logHeight₁`, `NumberField.logHeight₁_eq`, `logHeight₁_prod_le`, `logHeight₁_inv`, `logHeight₁_zpow`, `logHeight₁_eq_logHeight`, `logHeight₁_zero`, `logHeight₁_eq_log_mulHeight₁`
`mulHeight` 📖	CompOp	36 math math: `Projectivization.mulHeight_mk`, `mulHeight_sym2_le`, `mulHeight_mul_mulHeight`, `fun_mulHeight_zero`, `mulHeight_fun_prod_eq`, `mulHeight_mul_le`, `mulHeight_cons_cons_cons_zero`, `one_le_mulHeight`, `mulHeight_comp_le`, `NumberField.mulHeight_eq`, `mulHeight_cons_cons_zero`, `mulHeight_pow`, `mulHeight_comp_equiv`, `mulHeight_pos`, `mulHeight_swap`, `mulHeight_eq_mulHeight_restrict_support`, `mulHeight_cons_zero`, `mulHeight_zero`, `mulHeight_smul_eq_mulHeight`, `mulHeight_neg`, `mulHeight_eq`, `mulHeight_eq_one_of_subsingleton`, `mulHeight_eval_ge`, `logHeight_eq_log_mulHeight`, `mulHeight₁_eq_mulHeight`, `mulHeight_eval_le`, `fun_mulHeight_one`, `Finsupp.logHeight_eq_log_mulHeight`, `mulHeight₁_div_eq_mulHeight`, `mulHeight_sumElim_zero_eq`, `mulHeight_sym2_ge`, `mulHeight_eval_le'`, `mulHeight_eval_ge'`, `mulHeight_fun_mul_eq`, `mulHeight_linearMap_apply_le`, `mulHeight_one`
`mulHeight₁` 📖	CompOp	19 math math: `mulHeight₁_eq`, `mulHeight₁_zpow`, `mulHeight₁_pow`, `mulHeight₁_prod_le`, `mulHeight₁_add_le`, `one_le_mulHeight₁`, `mulHeight₁_sum_le`, `mulHeight₁_pos`, `mulHeight₁_sub_le`, `mulHeight₁_inv`, `mulHeight₁_mul_le`, `mulHeight₁_nonneg`, `mulHeight₁_eq_mulHeight`, `mulHeight₁_div_eq_mulHeight`, `mulHeight₁_zero`, `NumberField.mulHeight₁_eq`, `logHeight₁_eq_log_mulHeight₁`, `mulHeight₁_neg`, `mulHeight₁_one`
`totalWeight` 📖	CompOp	13 math math: `logHeight_eval_ge`, `logHeight₁_sum_le`, `logHeight₁_add_le`, `logHeight₁_sub_le`, `mulHeight₁_add_le`, `NumberField.totalWeight_eq_sum_mult`, `mulHeight₁_sum_le`, `mulHeight₁_sub_le`, `mulHeight_eval_ge`, `NumberField.totalWeight_pos`, `logHeight_linearMap_apply_le`, `NumberField.totalWeight_eq_finrank`, `mulHeight_linearMap_apply_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_comp_equiv` 📖	mathematical	—	`logHeight` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike`	—	`mulHeight_comp_equiv`
`logHeight_comp_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight`	—	`Real.log_le_log` `mulHeight_pos` `mulHeight_comp_le`
`logHeight_cons_cons_cons_zero` 📖	mathematical	—	`logHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_cons_cons_cons_zero`
`logHeight_cons_cons_zero` 📖	mathematical	—	`logHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_cons_cons_zero`
`logHeight_cons_zero` 📖	mathematical	—	`logHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_cons_zero`
`logHeight_eq_logHeight_restrict_support` 📖	mathematical	—	`logHeight` `Set.Elem` `Function.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Set` `Set.instMembership`	—	`mulHeight_eq_mulHeight_restrict_support`
`logHeight_eq_log_mulHeight` 📖	mathematical	—	`logHeight` `Real.log` `mulHeight`	—	—
`logHeight_eq_zero_of_subsingleton` 📖	mathematical	—	`logHeight` `Real` `Real.instZero`	—	`mulHeight_eq_one_of_subsingleton` `Real.log_one`
`logHeight_fun_mul_eq` 📖	mathematical	—	`logHeight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instAdd`	—	`ne_of_gt` `mulHeight_pos` `mulHeight_fun_mul_eq`
`logHeight_fun_prod_eq` 📖	mathematical	`Finite`	`logHeight` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Finset.univ` `Finset.sum` `Real` `Real.instAddCommMonoid`	—	`Finset.sum_congr` `Real.log_prod` `mulHeight_ne_zero` `mulHeight_fun_prod_eq`
`logHeight_mul_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instAdd`	—	`ne_of_gt` `mulHeight_pos` `Real.log_le_log` `mulHeight_mul_le`
`logHeight_neg` 📖	mathematical	—	`logHeight` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`mulHeight_neg`
`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.toPow` `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_sumElim_zero_eq` 📖	mathematical	—	`logHeight` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_sumElim_zero_eq`
`logHeight_swap` 📖	mathematical	—	`logHeight` `Matrix.vecCons` `Matrix.vecEmpty`	—	`mulHeight_swap`
`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` 📖	mathematical	—	`logHeight₁` `Real` `Real.instAdd` `Multiset.sum` `Real.instAddCommMonoid` `Multiset.map` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Real.posLog` `DFunLike.coe` `AbsoluteValue.funLike` `AdmissibleAbsValues.archAbsVal` `finsum` `Set.Elem` `AdmissibleAbsValues.nonarchAbsVal` `Set` `Set.instMembership`	—	`mulHeight₁_ne_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `Iff.not` `Multiset.prod_eq_zero_iff` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `left_ne_zero_of_mul` `mulHeight₁_eq` `Real.log_mul` `right_ne_zero_of_mul` `Real.log_multiset_prod` `Multiset.map_map` `Real.log_finprod` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Multiset.map_congr` `max_comm` `Real.posLog_eq_log_max_one` `AbsoluteValue.nonnegHomClass`
`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₁_mul_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight₁` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instAdd`	—	`ne_of_gt` `mulHeight₁_pos` `Real.log_le_log` `mulHeight₁_mul_le`
`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.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real` `Real.instMul` `Real.instNatCast`	—	`mulHeight₁_pow` `Real.log_pow`
`logHeight₁_prod_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight₁` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Finset.sum` `Real.instAddCommMonoid`	—	`Finset.sum_congr` `Real.log_prod` `ne_of_gt` `mulHeight₁_pos` `Real.log_le_log` `mulHeight₁_prod_le`
`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` `instReflLe` `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_comp_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight`	—	`eq_or_ne` `mulHeight_zero` `one_le_mulHeight` `instReflLe` `Function.ne_iff` `mulHeight_eq` `ciSup_le` `Finite.le_ciSup_of_le` `le_rfl` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Multiset.prod_map_le_prod_map₀` `Real.instZeroLEOneClass` `Real.iSup_nonneg_of_nonnegHomClass` `AbsoluteValue.nonnegHomClass` `finprod_le_finprod` `finprod_nonneg` `Multiset.prod_map_nonneg`
`mulHeight_cons_cons_cons_zero` 📖	mathematical	—	`mulHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_comp_equiv` `Matrix.cons_swap` `Matrix.cons_cons_comp_swap_zero_one` `mulHeight_cons_cons_zero`
`mulHeight_cons_cons_zero` 📖	mathematical	—	`mulHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_comp_equiv` `Matrix.cons_cons_comp_swap_zero_one` `mulHeight_cons_zero`
`mulHeight_cons_zero` 📖	mathematical	—	`mulHeight` `Matrix.vecCons` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`Matrix.cons_val_succ` `zero_lt_one` `Nat.instZeroLEOneClass` `mulHeight_comp_equiv` `mulHeight_sumElim_zero_eq` `Finite.of_fintype`
`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_eq_mulHeight_restrict_support` 📖	mathematical	—	`mulHeight` `Set.Elem` `Function.support` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Set` `Set.instMembership`	—	`Function.notMem_support` `Set.mem_compl_iff` `Subtype.prop` `mulHeight_comp_equiv` `mulHeight_sumElim_zero_eq` `Subtype.finite`
`mulHeight_eq_one_of_subsingleton` 📖	mathematical	—	`mulHeight` `Real` `Real.instOne`	—	`eq_or_ne` `mulHeight_zero` `Function.ne_iff` `mulHeight_smul_eq_mulHeight` `Finite.of_subsingleton` `inv_ne_zero` `inv_mul_cancel₀` `mulHeight_one`
`mulHeight_fun_mul_eq` 📖	mathematical	—	`mulHeight` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real` `Real.instMul`	—	`Function.ne_iff` `mul_ne_zero` `IsDomain.to_noZeroDivisors` `instIsDomain` `mulHeight_eq` `mul_mul_mul_comm` `Multiset.prod_map_mul` `finprod_mul_distrib` `Real.iSup_fun_mul_eq_iSup_mul_iSup_of_nonneg` `AbsoluteValue.nonnegHomClass` `AbsoluteValue.mulHomClass`
`mulHeight_fun_prod_eq` 📖	mathematical	`Finite`	`mulHeight` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Finset.univ` `Real` `Real.instCommMonoid`	—	`mulHeight_eq` `Finset.prod_ne_zero_iff` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `Multiset.map_congr` `map_prod` `MonoidWithZeroHomClass.toMonoidHomClass` `AbsoluteValue.monoidWithZeroHomClass` `Real.instIsDomain` `Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass` `AbsoluteValue.nonnegHomClass` `Multiset.prod_map_prod` `finprod_prod_comm` `Finset.prod_mul_distrib` `Finset.prod_congr`
`mulHeight_mul_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight` `Pi.instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instMul`	—	`isEmpty_or_nonempty` `mulHeight_eq_one_of_subsingleton` `IsEmpty.instSubsingleton` `mul_one` `instReflLe` `eq_or_ne` `MulZeroClass.zero_mul` `mulHeight_zero` `one_mul` `one_le_mulHeight` `MulZeroClass.mul_zero` `mulHeight_fun_mul_eq` `mulHeight_comp_le` `Finite.instProd`
`mulHeight_ne_zero` 📖	—	—	—	—	`LT.lt.ne'` `mulHeight_pos`
`mulHeight_neg` 📖	mathematical	—	`mulHeight` `Pi.instNeg` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing`	—	`eq_or_ne` `neg_zero` `mulHeight_zero` `mulHeight_eq` `neg_ne_zero` `Multiset.map_congr` `AddGroupSeminormClass.map_neg_eq_map` `AbsoluteValue.addGroupSeminormClass` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`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.toPow` `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` `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.hasFiniteMulSupport` `mul_mul_mul_comm` `AdmissibleAbsValues.product_formula` `one_mul`
`mulHeight_sumElim_zero_eq` 📖	mathematical	—	`mulHeight` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`eq_or_ne` `Sum.elim_zero_zero` `mulHeight_zero` `Function.ne_iff` `mulHeight_eq` `le_antisymm` `ciSup_le` `Finite.le_ciSup_of_le` `le_rfl` `AbsoluteValue.map_zero` `Real.iSup_nonneg_of_nonnegHomClass` `AbsoluteValue.nonnegHomClass` `Finite.instSum`
`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.toPow` `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` `instReflLe`
`mulHeight₁_div_eq_mulHeight` 📖	mathematical	—	`mulHeight₁` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `mulHeight` `Matrix.vecCons` `Matrix.vecEmpty`	—	`eq_or_ne` `div_zero` `mulHeight₁_zero` `mulHeight_cons_cons_zero` `mulHeight_eq_one_of_subsingleton` `mulHeight₁_eq_mulHeight` `mulHeight_smul_eq_mulHeight` `Finite.of_fintype` `Matrix.smul_cons` `mul_div_cancel₀` `mul_one` `Matrix.smul_empty`
`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₁_mul_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight₁` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instMul`	—	`mulHeight₁_eq_mulHeight` `Fintype.complete` `Matrix.cons_val_fin_one` `mul_one` `mulHeight_mul_le` `Finite.of_fintype`
`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` `AbsoluteValue.addGroupSeminormClass` `Real.instIsOrderedRing` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass`
`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.toPow` `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₁_prod_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight₁` `Finset.prod` `CommRing.toCommMonoid` `Field.toCommRing` `Real.instCommMonoid`	—	`Finset.induction` `mulHeight₁_one` `instReflLe` `Finset.prod_insert` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `mulHeight₁_pos` `mulHeight₁_mul_le`
`mulHeight₁_sub_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight₁` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real.instMul` `Monoid.toPow` `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.toPow` `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` `Function.HasFiniteMulSupport.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.toPow` `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` `instReflLe` `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` `Finite.le_ciSup_of_le` `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	7 math math: `Height.mulHeight₁_eq`, `Height.logHeight₁_eq`, `Height.mulHeight_eq`, `Height.mulHeightBound_eq`, `NumberField.prod_archAbsVal_eq`, `product_formula`, `NumberField.sum_archAbsVal_eq`
`nonarchAbsVal` 📖	CompOp	9 math math: `NumberField.prod_nonarchAbsVal_eq`, `Height.mulHeight₁_eq`, `Height.logHeight₁_eq`, `NumberField.sum_nonarchAbsVal_eq`, `Height.mulHeight_eq`, `mulSupport_finite`, `Height.mulHeightBound_eq`, `hasFiniteMulSupport`, `product_formula`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasFiniteMulSupport` 📖	mathematical	—	`Function.HasFiniteMulSupport` `Set.Elem` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `nonarchAbsVal` `Real.instOne` `DFunLike.coe` `AbsoluteValue.funLike` `Set` `Set.instMembership`	—	—
`isNonarchimedean` 📖	mathematical	`AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `Set` `Set.instMembership` `nonarchAbsVal`	`IsNonarchimedean` `Real` `Real.linearOrder` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike`	—	—
`mulSupport_finite` 📖	mathematical	—	`Function.HasFiniteMulSupport` `Set.Elem` `AbsoluteValue` `Real` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `nonarchAbsVal` `Real.instOne` `DFunLike.coe` `AbsoluteValue.funLike` `Set` `Set.instMembership`	—	`hasFiniteMulSupport`
`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