Theorems · Theorem · commutative algebra

MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero

∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R],
  ∑ a ∈ Finset.HasAntidiagonal.antidiagonal (Fintype.card σ),
      (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2 =
    0

Defined in

Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeCommRing