Theorems · Theorem · commutative algebra

MvPolynomial.supDegree_esymmAlgHomMonomial

∀ {R : Type u_3} {n m : ℕ} [inst : CommSemiring R] {r : R},
  r ≠ 0 →
    ∀ (t : Fin n →₀ ℕ),
      n ≤ m →
        ⇑(ofLex (AddMonoidAlgebra.supDegree (⇑toLex) (MvPolynomial.esymmAlgHomMonomial (Fin m) t r))) =
          (Fin.accumulate n m) ⇑t

Defined in: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Cited by: 2 results in Mathlib
Foundations: Depth 103 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites40

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
CommSemiringstatement and proof · cited by 10,911
Equivstatement · cited by 8,337
Finsuppstatement and proof · cited by 5,255
AddMonoidHomstatement · cited by 3,230
MvPolynomialproof · cited by 2,140
map_zeroproof · cited by 1,614
map_addproof · cited by 964
Finsupp.singleproof · cited by 943
Finsupp.supportproof · cited by 828
LT.lt.trans_leproof · cited by 678
Equiv.injectiveproof · cited by 464

Cited by2

Results whose statement or proof uses this declaration.

MvPolynomial.esymmAlgHom_fin_injectiveproof · cited by 2
MvPolynomial.esymmAlgHom_fin_bijectiveproof · cited by 1