Documentation Verification Report

Vieta

📁 Source: Mathlib/RingTheory/Polynomial/Vieta.lean

Statistics

Metric	Count
Definitions	0
Theorems `prod_X_add_C_coeff`, `esymm_neg`, `prod_X_add_C_coeff`, `prod_X_add_C_coeff'`, `prod_X_add_C_eq_sum_esymm`, `prod_X_sub_C_coeff`, `prod_X_sub_X_eq_sum_esymm`, `prod_C_add_X_eq_sum_esymm`, `prod_X_add_C_coeff`, `coeff_eq_esymm_roots_of_card`, `coeff_eq_esymm_roots_of_splits`	11
Total	11

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_X_add_C_coeff` 📖	mathematical	`card`	`Polynomial.coeff` `CommSemiring.toSemiring` `prod` `Polynomial` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `sum` `Finset` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `powersetCard`	—	`prod.eq_1` `Multiset.prod_X_add_C_coeff'` `esymm_map_val`

Multiset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`esymm_neg` 📖	mathematical	—	`esymm` `CommRing.toCommSemiring` `map` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne`	—	`esymm.eq_1` `sum_map_mul_left` `powersetCard_map` `map_map` `map_congr` `mem_powersetCard` `prod_replicate` `map_const` `map_id'` `prod_map_mul` `neg_one_mul`
`prod_X_add_C_coeff` 📖	mathematical	`card`	`Polynomial.coeff` `CommSemiring.toSemiring` `prod` `Polynomial` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `map` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `esymm`	—	`Polynomial.finset_sum_coeff` `Finset.sum_congr` `Polynomial.coeff_C_mul_X_pow` `Finset.sum_eq_single_of_mem` `Polynomial.ext_iff` `prod_X_add_C_eq_sum_esymm`
`prod_X_add_C_coeff'` 📖	mathematical	`card`	`Polynomial.coeff` `CommSemiring.toSemiring` `prod` `Polynomial` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `map` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `esymm`	—	`map_map` `prod_X_add_C_coeff` `card_map`
`prod_X_add_C_eq_sum_esymm` 📖	mathematical	—	`prod` `Polynomial` `CommSemiring.toSemiring` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `map` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.range` `card` `Polynomial.instMul` `esymm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`prod_map_add` `antidiagonal_eq_map_powerset` `map_map` `bind_powerset_len` `map_bind` `sum_bind` `Finset.sum_eq_multiset_sum` `Finset.range_val` `map_congr` `esymm.eq_1` `sum_hom'` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `sum_map_mul_right` `prod_hom'` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_const'` `card_sub` `mem_powersetCard` `prod_replicate` `map_id'` `Polynomial.X_pow_mul_C`
`prod_X_sub_C_coeff` 📖	mathematical	`card`	`Polynomial.coeff` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `prod` `Polynomial` `CommRing.toCommMonoid` `Polynomial.commRing` `map` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `esymm`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_map` `esymm_neg` `card_map` `prod_X_add_C_coeff`
`prod_X_sub_X_eq_sum_esymm` 📖	mathematical	—	`prod` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRing.toCommMonoid` `Polynomial.commRing` `map` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.range` `card` `Polynomial.instMul` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.instNeg` `Polynomial.instOne` `esymm`	—	`sub_eq_add_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_map` `Finset.sum_congr` `card_map` `esymm_neg` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `map_one` `MonoidHomClass.toOneHomClass` `mul_assoc` `prod_X_add_C_eq_sum_esymm`

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prod_C_add_X_eq_sum_esymm` 📖	mathematical	—	`Finset.prod` `Polynomial` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `Finset.univ` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `X` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Finset.range` `Fintype.card` `Polynomial.instMul` `esymm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`Multiset.card_map` `Finset.card_univ` `Finset.card_def` `Finset.sum_congr` `esymm_eq_multiset_esymm` `Multiset.map_map` `Multiset.map_congr` `Multiset.prod_X_add_C_eq_sum_esymm`
`prod_X_add_C_coeff` 📖	mathematical	`Fintype.card`	`Polynomial.coeff` `MvPolynomial` `CommSemiring.toSemiring` `commSemiring` `Finset.prod` `Polynomial` `CommSemiring.toCommMonoid` `Polynomial.commSemiring` `Finset.univ` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C` `X` `esymm`	—	`Multiset.card_map` `Finset.card_univ` `Finset.card_def` `esymm_eq_multiset_esymm` `Finset.prod_eq_multiset_prod` `Multiset.map_map` `Multiset.map_congr` `Multiset.prod_X_add_C_coeff`

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_eq_esymm_roots_of_card` 📖	mathematical	`Multiset.card` `roots` `natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`coeff` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Multiset.esymm`	—	`C_leadingCoeff_mul_prod_multiset_X_sub_C` `coeff_C_mul` `mul_assoc` `Multiset.prod_X_sub_C_coeff`
`coeff_eq_esymm_roots_of_splits` 📖	mathematical	`Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `natDegree`	`coeff` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `leadingCoeff` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `Multiset.esymm` `Semifield.toCommSemiring` `roots` `instIsDomain`	—	`coeff_eq_esymm_roots_of_card` `instIsDomain` `splits_iff_card_roots`

---

← Back to Index