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` `AddMonoidAlgebra.instMul` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddMonoidAlgebra.ring` `CommRing.toRing` `Finsupp.instAddMonoid` `esymm` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `AddMonoidAlgebra.zero` `Finsupp.instZero` `Finset.sum` `AddMonoidAlgebra.addAddCommMonoid` `Finset.filter` `Finset.HasAntidiagonal.antidiagonal` `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` `AddMonoidAlgebra.ring` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommRing.toRing` `Finsupp.instAddMonoid` `Nat.instAddMonoid` `AddMonoidAlgebra.instMul` `CommSemiring.toSemiring` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `AddMonoidAlgebra.zero` `Finsupp.instZero` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `esymm` `Finset.sum` `AddMonoidAlgebra.addAddCommMonoid` `Finset.filter` `Set` `Set.instMembership` `Set.Ioo` `Nat.instPreorder` `Set.decidableMemIoo` `Finset.HasAntidiagonal.antidiagonal` `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` `AddMonoidAlgebra.addAddCommMonoid` `Finsupp` `MulZeroClass.toZero` `Nat.instMulZeroClass` `CommSemiring.toSemiring` `Finset.HasAntidiagonal.antidiagonal` `Nat.instAddMonoid` `Finset.Nat.instHasAntidiagonal` `Fintype.card` `AddMonoidAlgebra.instMul` `Finsupp.instAdd` `AddMonoid.toAddZeroClass` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddMonoidAlgebra.semiring` `Finsupp.instAddMonoid` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `AddMonoidAlgebra.addAddCommGroup` `CommRing.toRing` `AddMonoidAlgebra.zero` `Finsupp.instZero` `esymm` `psum` `NonUnitalNonAssocSemiring.toMulZeroClass` `AddMonoidAlgebra.nonUnitalNonAssocSemiring`	—	`Finset.sum_filter_add_sum_filter_not` `Finset.sum_congr` `add_left_injective` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Finset.filter.congr_simp` `Finset.Nat.antidiagonal_filter_le_fst_of_le` `instReflLe` `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