Documentation Verification Report

CauchyBound

📁 Source: Mathlib/Analysis/Polynomial/CauchyBound.lean

Statistics

Metric	Count
Definitions `cauchyBound`	1
Theorems `norm_lt_cauchyBound`, `cauchyBound_C`, `cauchyBound_X`, `cauchyBound_X_add_C`, `cauchyBound_X_sub_C`, `cauchyBound_one`, `cauchyBound_smul`, `cauchyBound_zero`, `one_le_cauchyBound`	9
Total	10

Polynomial

Definitions

Name	Category	Theorems
`cauchyBound` 📖	CompOp	9 math math: `cauchyBound_smul`, `cauchyBound_C`, `cauchyBound_one`, `one_le_cauchyBound`, `cauchyBound_zero`, `cauchyBound_X_add_C`, `cauchyBound_X_sub_C`, `cauchyBound_X`, `IsRoot.norm_lt_cauchyBound`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cauchyBound_C` 📖	mathematical	—	`cauchyBound` `DFunLike.coe` `RingHom` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `NNReal` `instOneNNReal`	—	`natDegree_C` `Finset.sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `leadingCoeff_C` `zero_div` `zero_add`
`cauchyBound_X` 📖	mathematical	—	`cauchyBound` `X` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `NNReal` `instOneNNReal`	—	`natDegree_X` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Finset.sup_singleton` `coeff_X_zero` `nnnorm_zero` `Monic.leadingCoeff` `nnnorm_one` `NormedDivisionRing.to_normOneClass` `div_one` `zero_add`
`cauchyBound_X_add_C` 📖	mathematical	—	`cauchyBound` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `instAdd` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing` `instOneNNReal`	—	`natDegree_add_C` `natDegree_X` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `coeff_add` `Finset.sup_singleton` `coeff_X_zero` `coeff_C_zero` `zero_add` `leadingCoeff_X_add_C` `nnnorm_one` `NormedDivisionRing.to_normOneClass` `div_one`
`cauchyBound_X_sub_C` 📖	mathematical	—	`cauchyBound` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `instSub` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `semiring` `RingHom.instFunLike` `C` `NNReal` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instSemiringNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `instOneNNReal`	—	`natDegree_sub_C` `natDegree_X` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `coeff_sub` `Finset.sup_singleton` `coeff_X_zero` `coeff_C_zero` `zero_sub` `nnnorm_neg` `leadingCoeff_X_sub_C` `nnnorm_one` `NormedDivisionRing.to_normOneClass` `div_one`
`cauchyBound_one` 📖	mathematical	—	`cauchyBound` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `instOne` `NNReal` `instOneNNReal`	—	`cauchyBound_C`
`cauchyBound_smul` 📖	mathematical	—	`cauchyBound` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `SMulZeroClass.toSMul` `instZero` `smulZeroClass` `DistribSMul.toSMulZeroClass` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `NormedRing.toRing` `NormedDivisionRing.toNormedRing` `NonUnitalNonAssocSemiring.toDistribSMul` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	—	`natDegree_smul_of_smul_regular` `IsLeftRegular.isSMulRegular` `IsRegular.left` `IsRegular.of_ne_zero` `IsDomain.toIsCancelMulZero` `DivisionRing.isDomain` `coeff_smul` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `leadingCoeff_smul_of_smul_regular` `AddRightCancelSemigroup.toIsRightCancelAdd` `mul_div_mul_left`
`cauchyBound_zero` 📖	mathematical	—	`cauchyBound` `Polynomial` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing` `instZero` `NNReal` `instOneNNReal`	—	`nnnorm_zero` `Finset.sup_empty` `bot_eq_zero'` `NNReal.instCanonicallyOrderedAdd` `div_zero` `zero_add`
`one_le_cauchyBound` 📖	mathematical	—	`NNReal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrderNNReal` `instOneNNReal` `cauchyBound`	—	`covariant_swap_add_of_covariant_add` `NNReal.addLeftMono` `IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT` `AddRightCancelSemigroup.toIsRightCancelAdd` `contravariant_swap_add_of_contravariant_add` `NNReal.addLeftReflectLT` `NNReal.instCanonicallyOrderedAdd`

Polynomial.IsRoot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`norm_lt_cauchyBound` 📖	mathematical	`Polynomial.IsRoot` `DivisionSemiring.toSemiring` `DivisionRing.toDivisionSemiring` `NormedDivisionRing.toDivisionRing`	`NNReal` `Preorder.toLT` `PartialOrder.toPreorder` `instPartialOrderNNReal` `NNNorm.nnnorm` `SeminormedAddGroup.toNNNorm` `SeminormedAddCommGroup.toSeminormedAddGroup` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalNormedRing.toNonUnitalSeminormedRing` `NormedRing.toNonUnitalNormedRing` `NormedDivisionRing.toNormedRing` `Polynomial.cauchyBound`	—	`mul_div_cancel_left₀` `GroupWithZero.toMulDivCancelClass` `div_le_div_of_nonneg_right` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `NNReal.instIsStrictOrderedRing` `le_of_eq` `nnnorm_mul` `NormedDivisionRing.toNormMulClass` `nnnorm_pow` `NormedDivisionRing.to_normOneClass` `nnnorm_neg` `Finset.sum_insert` `Finset.range_add_one` `Polynomial.eval_eq_sum_range` `def` `le_of_lt` `lt_of_le_of_ne'` `zero_le` `NNReal.instCanonicallyOrderedAdd` `nnnorm_sum_le` `Finset.sum_congr` `Finset.sum_le_sum` `NNReal.addLeftMono` `mul_le_mul_left` `covariant_swap_mul_of_covariant_mul` `NNReal.mulLeftMono` `Polynomial.cauchyBound.eq_1` `add_tsub_cancel_right` `NNReal.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `NNReal.addLeftReflectLT` `Mathlib.Tactic.FieldSimp.le_eq_cancel_le` `PosMulStrictMono.toPosMulMono` `LinearOrderedCommMonoidWithZero.toPosMulStrictMono` `PosMulStrictMono.toPosMulReflectLE` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `zero_lt_one` `LinearOrderedCommMonoidWithZero.toZeroLeOneClass` `NeZero.one` `GroupWithZero.toNontrivial` `Finset.le_sup` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₂` `one_ne_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` `eq_or_ne` `lt_of_le_of_ne` `tsub_self` `MulZeroClass.zero_mul` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `one_pow` `Finset.sum_const` `Finset.card_range` `nsmul_eq_mul` `lt_or_gt_of_ne` `LT.lt.trans_le` `tsub_add_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `LT.lt.le` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `ne_of_gt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `IsStrictOrderedRing.toZeroLEOneClass` `lt_trans` `Mathlib.Meta.Positivity.pos_of_isNat` `NNReal.instIsOrderedRing` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `Mathlib.Tactic.FieldSimp.NF.cons_ne_zero` `Right.add_pos_of_nonneg_of_pos` `covariant_swap_add_of_covariant_add` `Mathlib.Tactic.Ring.cast_pos` `add_le_add_left` `geom_sum_of_one_lt` `LT.lt.false` `tsub_eq_zero_iff_le` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `add_lt_add_left` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `div_lt_div_of_pos_right` `mul_lt_mul_of_pos_left` `LT.lt.trans` `Mathlib.Tactic.Contrapose.contrapose₃`

---

← Back to Index