Documentation Verification Report

GaussLucas

📁 Source: Mathlib/Analysis/Complex/Polynomial/GaussLucas.lean

Statistics

Metric	Count
Definitions `derivRootWeight`	1
Theorems `derivRootWeight_nonneg`, `eq_centerMass_of_eval_derivative_eq_zero`, `rootSet_derivative_subset_convexHull_rootSet`, `sum_derivRootWeight_pos`	4
Total	5

Polynomial

Definitions

Name	Category	Theorems
`derivRootWeight` 📖	CompOp	3 math math: `eq_centerMass_of_eval_derivative_eq_zero`, `sum_derivRootWeight_pos`, `derivRootWeight_nonneg`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivRootWeight_nonneg` 📖	mathematical	—	`Real` `Real.instLE` `Real.instZero` `derivRootWeight`	—	`Function.update_apply` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `div_nonneg` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `Even.pow_nonneg` `IsStrictOrderedRing.toIsOrderedRing` `AddGroup.existsAddOfLE` `Nat.instAtLeastTwoHAddOfNat` `even_two_mul`
`eq_centerMass_of_eval_derivative_eq_zero` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Complex` `Complex.instSemiring` `eval` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `Complex.instZero`	`Finset.centerMass` `Real` `Real.instField` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `Multiset.toFinset` `Complex.instDecidableEq` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField` `derivRootWeight`	—	`instIsDomain` `Finset.sum_congr` `Finset.sum_eq_single` `Pi.single_eq_of_ne` `zero_smul` `Pi.single_eq_same` `sub_self` `smul_zero` `map_sum` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `Complex.instCharZero` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `RingHom.instRingHomClass` `sub_ne_zero` `Complex.ofReal_div` `Complex.ofReal_pow` `map_sub` `one_div` `nsmul_eq_mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_natCast` `map_inv₀` `RingHomClass.toMonoidWithZeroHomClass` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `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₃` `mul_one` `Mathlib.Tactic.FieldSimp.NF.div_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` `Mathlib.Tactic.FieldSimp.eq_div_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div'` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Finset.sum_multiset_map_count` `count_roots` `Splits.eval_derivative_div_eval_of_ne_zero` `IsAlgClosed.splits` `Complex.isAlgClosed` `zero_div` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `Finset.centerMass.eq_1` `Finset.sum_smul` `inv_smul_smul₀` `LT.lt.ne'` `sum_derivRootWeight_pos` `sub_add_cancel` `AddRightCancelSemigroup.toIsRightCancelAdd`
`rootSet_derivative_subset_convexHull_rootSet` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Complex` `Complex.instSemiring`	`Set` `Set.instHasSubset` `rootSet` `Complex.commRing` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `semiring` `module` `Semiring.toModule` `LinearMap.instFunLike` `derivative` `instIsDomain` `Field.toSemifield` `Complex.instField` `Algebra.id` `CommRing.toCommSemiring` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `Complex.instNormedAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex`	—	`instIsDomain` `eq_centerMass_of_eval_derivative_eq_zero` `coe_aeval_eq_eval` `mem_rootSet` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Finset.centerMass_mem_convexHull` `Real.instIsStrictOrderedRing` `sum_derivRootWeight_pos`
`sum_derivRootWeight_pos` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Complex` `Complex.instSemiring`	`Real` `Real.instLT` `Real.instZero` `Finset.sum` `Real.instAddCommMonoid` `Multiset.toFinset` `Complex.instDecidableEq` `roots` `Complex.commRing` `instIsDomain` `Field.toSemifield` `Complex.instField` `derivRootWeight`	—	`instIsDomain` `Finset.sum_congr` `Finset.sum_pi_single'` `Real.instZeroLEOneClass` `NeZero.charZero_one` `RCLike.charZero_rclike` `Finset.sum_pos` `Real.instIsOrderedCancelAddMonoid` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `Real.instIsOrderedRing` `Real.instNontrivial` `AddGroup.existsAddOfLE` `Multiset.toFinset_nonempty` `Splits.roots_ne_zero` `IsAlgClosed.splits` `Complex.isAlgClosed` `pos_iff_ne_zero` `Nat.instCanonicallyOrderedAdd` `natDegree_pos_iff_degree_pos`

---

← Back to Index