Theorems · Theorem · field theory

Polynomial.hasseDeriv_mul

∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (f g : Polynomial R),
  (Polynomial.hasseDeriv k) (f * g) =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, (Polynomial.hasseDeriv ij.1) f * (Polynomial.hasseDeriv ij.2) g

Defined in: Mathlib.Algebra.Polynomial.HasseDeriv
Cited by: 0 results in Mathlib
Foundations: Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Semiring

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites41

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
RingHom.idstatement and proof · cited by 18,349
Semiringstatement and proof · cited by 13,802
LinearMapstatement and proof · cited by 10,215
Polynomialstatement and proof · cited by 5,681
Finset.sumstatement and proof · cited by 5,195
AddMonoidHomproof · cited by 3,230
Finset.sum_congrproof · cited by 2,323
MulZeroClass.mul_zeroproof · cited by 2,091
Nat.cast_zeroproof · cited by 1,870
mul_assocproof · cited by 1,667
MulZeroClass.zero_mulproof · cited by 1,625

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.