Documentation Verification Report

NewtonIdentities

📁 Source: Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean

Statistics

Metric	Count
Definitions	0
Theorems `mul_esymm_eq_sum`, `psum_eq_mul_esymm_sub_sum`, `sum_antidiagonal_card_esymm_psum_eq_zero`	3
Total	3

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mul_esymm_eq_sum` 📖	mathematical	—	`MvPolynomial` `CommRing.toCommSemiring` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `esymm` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `psum`	—	`sub_eq_zero` `sub_eq_add_neg` `neg_mul_eq_neg_mul` `neg_eq_neg_one_mul` `pow_one` `pow_add` `add_comm` `left_distrib` `Distrib.leftDistribClass` `Finset.sum_disjUnion` `neg_one_pow_mul_eq_zero_iff`
`psum_eq_mul_esymm_sub_sum` 📖	mathematical	—	`psum` `CommRing.toCommSemiring` `MvPolynomial` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRingMvPolynomial` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `AddMonoidWithOne.toNatCast` `esymm` `Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Finset.filter` `Set` `Set.instMembership` `Set.Ioo` `Nat.instPreorder` `Set.decidableMemIoo` `Preorder.toLT` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal`	—	`Finset.sum_congr` `Finset.filter.congr_simp` `mul_esymm_eq_sum` `Finset.sum_filter_add_sum_filter_not` `left_distrib` `Distrib.leftDistribClass` `add_sub_cancel_left` `Finset.ext` `Finset.mem_filter` `Finset.HasAntidiagonal.mem_antidiagonal` `Finset.mem_singleton` `zero_add` `Finset.filter_filter` `pow_zero` `esymm_zero` `mul_one` `one_mul` `Finset.sum_singleton` `mul_sub_left_distrib` `Even.neg_one_pow`
`sum_antidiagonal_card_esymm_psum_eq_zero` 📖	mathematical	—	`Finset.sum` `MvPolynomial` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRingMvPolynomial` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Fintype.card` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `commSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `esymm` `psum` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.sum_filter_add_sum_filter_not` `Finset.sum_congr` `add_left_injective` `AddRightCancelSemigroup.toIsRightCancelAdd` `Finset.filter.congr_simp` `Finset.Nat.antidiagonal_filter_le_fst_of_le` `tsub_self` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Finset.antidiagonal_zero` `Finset.map_singleton` `zero_add` `Finset.sum_singleton` `psum_zero` `mul_add` `Distrib.leftDistribClass` `mul_comm` `Odd.neg_one_pow` `neg_mul` `one_mul` `add_neg_cancel`

---

← Back to Index