Documentation Verification Report

MvPolynomial

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

Statistics

Metric	Count
Definitions `mulHeightBound`	1
Theorems `eval_mvPolynomial_le`, `iSup_abv_linearMap_apply_le`, `abs_logHeight_sym2_sub_le`, `logHeight_eval_ge`, `logHeight_eval_ge'`, `logHeight_eval_le`, `logHeight_eval_le'`, `logHeight_linearMap_apply_le`, `logHeight_sym2_ge`, `logHeight_sym2_le`, `max_mulHeightBound_zero_one_eq_one`, `mulHeightBound_eq`, `mulHeight_eval_ge`, `mulHeight_eval_ge'`, `mulHeight_eval_le`, `mulHeight_eval_le'`, `mulHeight_linearMap_apply_le`, `mulHeight_mul_mulHeight`, `mulHeight_sym2_ge`, `mulHeight_sym2_le`, `apply_sum_le`, `eval_mvPolynomial_le`, `iSup_abv_linearMap_apply_le`	23
Total	24

AbsoluteValue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eval_mvPolynomial_le` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `funLike` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instMul` `Finsupp.sum` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Real.instAddCommMonoid` `Monoid.toPow` `Real.instMonoid` `iSup` `Real.instSupSet`	—	`MvPolynomial.eval_eq` `MvPolynomial.sum_def` `Finset.sum_mul` `le_imp_le_of_le_of_le` `sum_le` `Real.instIsOrderedRing` `le_refl` `Finset.sum_congr` `map_mul` `map_prod` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Real.instIsStrictOrderedRing` `Finset.prod_congr` `map_pow` `Real.instIsDomain` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support` `Finset.prod_pow_eq_pow_sum` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `NonnegHomClass.apply_nonneg` `nonnegHomClass` `pow_le_pow_left₀` `IsOrderedRing.toMulPosMono` `Finite.le_ciSup`
`iSup_abv_linearMap_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `iSup` `Real.instSupSet` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `funLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Real.instMul` `Real.instNatCast` `Nat.card`	—	`isEmpty_or_nonempty` `Real.iSup_of_isEmpty` `Nat.card_eq_fintype_card` `Prod.isEmpty_left` `MulZeroClass.mul_zero` `MulZeroClass.zero_mul` `instReflLe` `ciSup_le` `le_imp_le_of_le_of_le` `sum_le` `Real.instIsOrderedRing` `le_refl` `Finset.sum_congr` `map_mul` `mulHomClass` `Finset.sum_le_sum` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Finite.le_ciSup_of_le` `Finite.instProd` `Finite.of_fintype` `le_rfl` `NonnegHomClass.apply_nonneg` `nonnegHomClass` `Real.iSup_nonneg_of_nonnegHomClass` `Finset.sum_const` `nsmul_eq_mul` `mul_assoc` `Finset.card_univ`

Height

Definitions

Name	Category	Theorems
`mulHeightBound` 📖	CompOp	6 math math: `logHeight_eval_ge`, `mulHeight_eval_ge`, `mulHeightBound_eq`, `mulHeight_eval_le`, `logHeight_eval_le`, `max_mulHeightBound_zero_one_eq_one`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`abs_logHeight_sym2_sub_le` 📖	mathematical	—	`Real` `Real.instLE` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub` `logHeight` `Matrix.vecCons` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Matrix.vecEmpty` `Real.instAdd`	—	`logHeight_sym2_le` `logHeight_sym2_ge`
`logHeight_eval_ge` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`Real` `Real.instLE` `Real.instAdd` `Real.instNeg` `Real.log` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.card` `totalWeight` `Real.instMax` `mulHeightBound` `Real.instOne` `logHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`isEmpty_or_nonempty` `Nat.card_eq_fintype_card` `Fintype.card_eq_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Unique.instSubsingleton` `Prod.isEmpty_right` `max_mulHeightBound_zero_one_eq_one` `mul_one` `Real.log_pow` `Real.log_zero` `MulZeroClass.mul_zero` `neg_zero` `mulHeight_zero` `Real.log_one` `add_zero` `MvPolynomial.eval_zero` `mulHeight_eq_one_of_subsingleton` `IsEmpty.instSubsingleton` `instReflLe` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `ne_of_gt` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `lt_of_le_of_ne'` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Real.instIsOrderedRing` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `mulHeight_pos` `Real.log_le_log` `mulHeight_eval_ge`
`logHeight_eval_ge'` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLE` `Real.instAdd` `Real.instMul` `Real.instNatCast` `logHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`logHeight_eval_ge`
`logHeight_eval_le` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLE` `logHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instAdd` `Real.log` `Real.instMax` `mulHeightBound` `Real.instOne` `Real.instMul` `Real.instNatCast`	—	`ne_of_gt` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `mulHeight_pos` `Real.log_le_log` `mulHeight_eval_le`
`logHeight_eval_le'` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLE` `logHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instAdd` `Real.instMul` `Real.instNatCast`	—	`logHeight_eval_le`
`logHeight_linearMap_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Real.instAdd` `Real.instMul` `Real.instNatCast` `totalWeight` `Real.log` `Nat.card`	—	`isEmpty_or_nonempty` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `logHeight_nonneg` `Finite.instProd` `Finite.of_fintype` `Finset.sum_congr` `Finset.univ_eq_empty` `fun_logHeight_zero` `Nat.card_eq_fintype_card` `Fintype.card_eq_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Real.log_zero` `MulZeroClass.mul_zero` `logHeight_eq_zero_of_subsingleton` `IsEmpty.instSubsingleton` `Prod.isEmpty_right` `add_zero` `instReflLe` `isReduced_of_noZeroDivisors` `NormMulClass.toNoZeroDivisors` `NormedDivisionRing.toNormMulClass` `Real.instNontrivial` `ne_of_gt` `mulHeight_pos` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `lt_of_le_of_ne'` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Real.instIsOrderedRing` `IsOrderedRing.toPosMulMono` `Nat.cast_nonneg'` `Real.instZeroLEOneClass` `Real.log_le_log` `mulHeight_linearMap_apply_le`
`logHeight_sym2_ge` 📖	mathematical	—	`Real` `Real.instLE` `Real.instAdd` `logHeight` `Matrix.vecCons` `Matrix.vecEmpty` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd`	—	`mulHeight_sym2_ge` `ne_of_gt` `mulHeight_pos` `Finite.of_fintype` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.log_le_log`
`logHeight_sym2_le` 📖	mathematical	—	`Real` `Real.instLE` `logHeight` `Matrix.vecCons` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Matrix.vecEmpty` `Real.instAdd`	—	`mulHeight_sym2_le` `ne_of_gt` `mulHeight_pos` `Finite.of_fintype` `mul_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.log_le_log`
`max_mulHeightBound_zero_one_eq_one` 📖	mathematical	—	`Real` `Real.instMax` `mulHeightBound` `Pi.instZero` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring` `Finsupp` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Real.instOne`	—	`Multiset.map_congr` `AbsoluteValue.map_zero` `Real.iSup_of_isEmpty` `Finset.instIsEmpty` `sup_of_le_right` `Real.instZeroLEOneClass` `Real.iSup_const_zero` `Multiset.map_const'` `Multiset.prod_replicate` `zero_pow_eq` `isEmpty_or_nonempty` `one_mul` `finprod_zero_le_one` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `MulZeroClass.zero_mul` `ciSup_const` `finprod_one` `mul_one`
`mulHeightBound_eq` 📖	mathematical	—	`mulHeightBound` `Real` `Real.instMul` `Multiset.prod` `Real.instCommMonoid` `Multiset.map` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `iSup` `Real.instSupSet` `Finsupp.sum` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Real.instAddCommMonoid` `DFunLike.coe` `AbsoluteValue.funLike` `AdmissibleAbsValues.archAbsVal` `finprod` `Set.Elem` `AdmissibleAbsValues.nonarchAbsVal` `Real.instMax` `Finset` `SetLike.instMembership` `Finset.instSetLike` `MvPolynomial.support` `Set` `Set.instMembership` `MvPolynomial.coeff` `Real.instOne`	—	—
`mulHeight_eval_ge` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `DFunLike.coe` `RingHom` `MvPolynomial` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring`	`Real` `Real.instLE` `Real.instMul` `Real.instInv` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.card` `totalWeight` `Real.instMax` `mulHeightBound` `Real.instOne` `mulHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`isEmpty_or_nonempty` `Nat.card_eq_fintype_card` `Fintype.card_eq_zero` `CharP.cast_eq_zero` `CharP.ofCharZero` `RCLike.charZero_rclike` `Unique.instSubsingleton` `Prod.isEmpty_right` `max_mulHeightBound_zero_one_eq_one` `mul_one` `mulHeight_zero` `one_pow` `MvPolynomial.eval_zero` `mulHeight_eq_one_of_subsingleton` `IsEmpty.instSubsingleton` `mulHeight_pow` `mulHeight_linearMap_apply_le` `inv_mul_le_iff₀` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `Nat.cast_zero` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Nat.card_pos` `Finite.of_fintype` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mul_le_mul_iff_left₀` `IsOrderedRing.toMulPosMono` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `mulHeight_pos` `pow_add` `add_comm` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_right` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `mulHeight_eval_le` `Finite.instProd` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Nat.cast_nonneg'` `le_of_lt` `Eq.le` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul`
`mulHeight_eval_ge'` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `mulHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval`	—	`isEmpty_or_nonempty` `zero_lt_one` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `mulHeight_zero` `one_pow` `mul_one` `MvPolynomial.eval_zero` `mulHeight_eq_one_of_subsingleton` `IsEmpty.instSubsingleton` `instReflLe` `Nat.card_pos` `Finite.of_fintype` `inv_pos_of_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `mul_pos` `pow_pos` `IsStrictOrderedRing.toZeroLEOneClass` `Nat.cast_pos'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mulHeight_eval_ge`
`mulHeight_eval_le` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLE` `mulHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instMul` `Real.instMax` `mulHeightBound` `Real.instOne` `Monoid.toPow` `Real.instMonoid`	—	`eq_or_ne` `MvPolynomial.eval_zero` `mulHeight_zero` `one_pow` `mul_one` `le_max_of_le_left` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `le_max_right` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `mulHeight_pos` `one_mul` `one_le_pow₀` `Real.instZeroLEOneClass` `IsOrderedRing.toPosMulMono` `one_le_mulHeight` `Real.iSup_nonneg` `Finsupp.sum_nonneg'` `Real.instIsOrderedAddMonoid` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `Multiset.prod_map_nonneg` `Real.iSup_nonneg_of_nonnegHomClass` `finprod_nonneg` `pow_nonneg` `Finite.le_ciSup` `mulHeight_eq` `le_max_left` `IsOrderedRing.toZeroLEOneClass` `mul_nonneg` `mul_pow` `mul_mul_mul_comm` `mul_le_mul` `Multiset.prod_map_pow` `Multiset.prod_map_mul` `Multiset.prod_map_le_prod_map₀` `Real.iSup_le` `AbsoluteValue.eval_mvPolynomial_le` `Function.ne_iff` `finprod_pow` `finprod_mul_distrib` `Function.HasFiniteMulSupport.fun_pow` `finprod_le_finprod` `Function.HasFiniteMulSupport.fun_mul` `IsNonarchimedean.eval_mvPolynomial_le` `AdmissibleAbsValues.isNonarchimedean` `Subtype.prop` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one`
`mulHeight_eval_le'` 📖	mathematical	`MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring` `Field.toSemifield`	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `mulHeight` `DFunLike.coe` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `Field.toSemifield` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instMul` `Monoid.toPow` `Real.instMonoid`	—	`lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `mulHeight_eval_le`
`mulHeight_linearMap_apply_le` 📖	mathematical	—	`Real` `Real.instLE` `mulHeight` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instNatCast` `Nat.card` `totalWeight`	—	`Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `RCLike.charZero_rclike` `Nat.card_pos` `Finite.of_fintype` `one_le_mulHeight` `Finite.instProd` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Nat.cast_nonneg'` `mul_nonneg` `mulHeight_pos` `isEmpty_or_nonempty` `mulHeight_eq_one_of_subsingleton` `IsEmpty.instSubsingleton` `Prod.isEmpty_left` `mul_one` `eq_or_ne` `mulHeight_zero` `Finset.sum_congr` `MulZeroClass.zero_mul` `Finset.sum_const_zero` `fun_mulHeight_zero` `Nat.card_eq_fintype_card` `MulZeroClass.mul_zero` `mulHeight_eq` `mul_mul_mul_comm` `mul_assoc` `Multiset.prod_map_mul` `Multiset.prod_replicate` `totalWeight.eq_1` `Multiset.map_const'` `Multiset.prod_map_le_prod_map₀` `Real.iSup_nonneg_of_nonnegHomClass` `AbsoluteValue.nonnegHomClass` `mul_comm` `AbsoluteValue.iSup_abv_linearMap_apply_le` `finprod_mul_distrib` `finprod_le_finprod` `Function.HasFiniteMulSupport.fun_mul` `IsNonarchimedean.iSup_abv_linearMap_apply_le` `AdmissibleAbsValues.isNonarchimedean` `Subtype.prop` `finprod_nonneg` `Multiset.prod_map_nonneg`
`mulHeight_mul_mulHeight` 📖	mathematical	—	`Real` `Real.instMul` `mulHeight` `Matrix.vecCons` `Matrix.vecEmpty` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	—	`mulHeight_fun_mul_eq` `Finite.of_fintype` `Fintype.complete` `zero_add` `MulZeroClass.mul_zero` `add_zero` `Matrix.cons_val_fin_one` `mul_one` `mulHeight_comp_equiv`
`mulHeight_sym2_ge` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `Real.instMul` `mulHeight` `Matrix.vecCons` `Matrix.vecEmpty` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd`	—	`Fintype.complete` `Matrix.cons_val'` `Matrix.cons_val_fin_one` `mulHeight_eval_ge'` `Finite.of_fintype` `mul_assoc` `mulHeight_mul_mulHeight` `MvPolynomial.eval_X` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `pow_one` `Finset.sum_congr` `Fin.sum_univ_three` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `MulZeroClass.zero_mul` `add_zero` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_mul` `Mathlib.Tactic.Ring.mul_add` `Mathlib.Tactic.Ring.mul_pf_left` `Mathlib.Tactic.Ring.mul_pf_right` `Mathlib.Tactic.Ring.one_mul` `Mathlib.Tactic.Ring.mul_zero` `Mathlib.Tactic.Ring.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.mul_pp_pf_overlap` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `Mathlib.Meta.NormNum.isNat_add` `Mathlib.Meta.NormNum.IsNat.of_raw` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.cast_pos` `Mathlib.Meta.NormNum.isNat_ofNat` `Mathlib.Tactic.Ring.pow_add` `Mathlib.Tactic.Ring.single_pow` `Mathlib.Tactic.Ring.mul_pow` `Mathlib.Tactic.Ring.one_pow` `Mathlib.Tactic.Ring.pow_zero` `zero_add` `map_neg` `neg_mul` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `Mathlib.Tactic.Ring.add_pf_add_gt` `Mathlib.Tactic.Ring.neg_congr` `Mathlib.Tactic.Ring.neg_add` `Mathlib.Tactic.Ring.neg_mul` `Mathlib.Tactic.Ring.neg_one_mul` `Mathlib.Meta.NormNum.IsInt.to_raw_eq` `Mathlib.Meta.NormNum.isInt_mul` `Mathlib.Meta.NormNum.IsInt.of_raw` `Mathlib.Meta.NormNum.IsNat.to_isInt` `Mathlib.Tactic.Ring.neg_zero` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add`
`mulHeight_sym2_le` 📖	mathematical	—	`Real` `Real.instLT` `Real.instZero` `Real.instLE` `mulHeight` `Matrix.vecCons` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Distrib.toAdd` `Matrix.vecEmpty` `Real.instMul`	—	`Fintype.complete` `mulHeight_eval_le'` `Finite.of_fintype` `mulHeight_zero` `mul_one` `MulZeroClass.zero_mul` `add_zero` `le_imp_le_of_le_of_le` `le_refl` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `one_le_mulHeight` `le_of_lt` `lt_max_of_lt_left` `MulZeroClass.mul_zero` `mul_assoc` `mulHeight_mul_mulHeight` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `le_max_left` `mulHeight_pos` `MvPolynomial.eval_X` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `pow_one`

IsNonarchimedean

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_sum_le` 📖	mathematical	`IsNonarchimedean` `Real` `Real.linearOrder` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `DFunLike.coe`	`Real` `Real.instLE` `DFunLike.coe` `Finset.sum` `iSup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `Real.instSupSet`	—	`Finset.induction` `map_zero` `Real.iSup_of_isEmpty` `Finset.instIsEmpty` `instReflLe` `Finset.sum_insert` `le_imp_le_of_le_of_le` `le_refl` `sup_le_sup` `max_le` `Finite.le_ciSup_of_le` `Finite.of_fintype` `Finset.mem_insert_self` `le_rfl` `isEmpty_or_nonempty` `Real.iSup_nonneg_of_nonnegHomClass` `ciSup_le` `Finset.mem_insert_of_mem` `Subtype.prop`
`eval_mvPolynomial_le` 📖	mathematical	`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` `MvPolynomial.IsHomogeneous` `Semifield.toCommSemiring`	`Real` `Real.instLE` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `RingHom` `MvPolynomial` `Semifield.toCommSemiring` `AddMonoidAlgebra.nonAssocSemiring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAddZeroClass` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `MvPolynomial.eval` `Real.instMul` `iSup` `Finset` `SetLike.instMembership` `Finset.instSetLike` `MvPolynomial.support` `Real.instSupSet` `MvPolynomial.coeff` `Monoid.toPow` `Real.instMonoid`	—	`eq_or_ne` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `AbsoluteValue.map_zero` `Real.iSup_of_isEmpty` `Finset.instIsEmpty` `MulZeroClass.zero_mul` `instReflLe` `MvPolynomial.eval_eq` `finset_image_add_of_nonempty` `MvPolynomial.support_nonempty` `le_imp_le_of_le_of_le` `le_refl` `AbsoluteValue.map_mul` `AbsoluteValue.map_prod` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Real.instIsStrictOrderedRing` `Finset.prod_congr` `AbsoluteValue.map_pow` `Real.instIsDomain` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Finite.le_ciSup_of_le` `Finite.of_fintype` `le_rfl` `MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support` `Finset.prod_pow_eq_pow_sum` `Finset.prod_le_prod` `Real.instZeroLEOneClass` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `NonnegHomClass.apply_nonneg` `AbsoluteValue.nonnegHomClass` `pow_le_pow_left₀` `Finite.le_ciSup` `Finset.prod_nonneg` `Real.iSup_nonneg_of_nonnegHomClass`
`iSup_abv_linearMap_apply_le` 📖	mathematical	`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`	`Real` `Real.instLE` `iSup` `Real.instSupSet` `DFunLike.coe` `AbsoluteValue` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Real.semiring` `Real.partialOrder` `AbsoluteValue.funLike` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Finset.univ` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Real.instMul`	—	`isEmpty_or_nonempty` `Finset.sum_congr` `Finset.univ_eq_empty` `AbsoluteValue.map_zero` `Real.iSup_const_zero` `Real.iSup_of_isEmpty` `Prod.isEmpty_right` `MulZeroClass.mul_zero` `instReflLe` `Prod.isEmpty_left` `MulZeroClass.zero_mul` `ciSup_le` `le_imp_le_of_le_of_le` `apply_sum_le` `AbsoluteValue.nonnegHomClass` `AbsoluteValue.zeroHomClass` `le_refl` `map_mul` `AbsoluteValue.mulHomClass` `Function.Surjective.iSup_comp` `Finset.mem_univ` `mul_le_mul` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `IsOrderedRing.toMulPosMono` `Finite.le_ciSup_of_le` `Finite.instProd` `Finite.of_fintype` `le_rfl` `NonnegHomClass.apply_nonneg` `Real.iSup_nonneg_of_nonnegHomClass`

---

← Back to Index