Theorems · Theorem · commutative algebra

PowerSeries.coeff_mul

∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (φ ψ : PowerSeries R),
  (PowerSeries.coeff n) (φ * ψ) =
    ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, (PowerSeries.coeff p.1) φ * (PowerSeries.coeff p.2) ψ

Defined in: Mathlib.RingTheory.PowerSeries.Basic
Cited by: 29 results in Mathlib
Foundations: Depth 88 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.

Cites17

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 · cited by 18,349
Semiringstatement and proof · cited by 13,802
Finsetproof · cited by 13,712
LinearMapstatement · cited by 10,215
Finsuppproof · cited by 5,255
Finset.sumstatement and proof · cited by 5,195
Finsupp.singleproof · cited by 943
PowerSeriesstatement and proof · cited by 797
PowerSeries.coeffstatement and proof · cited by 324
MvPowerSeries.coeffproof · cited by 273
Finset.HasAntidiagonal.antidiagonalstatement and proof · cited by 218

Cited by29

Results whose statement or proof uses this declaration.

PowerSeries.coeff_X_pow_mul'proof · cited by 7
PowerSeries.le_order_mulproof · cited by 5
PowerSeries.trunc_trunc_mulproof · cited by 4
PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_idealproof · cited by 4
Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_evalproof · cited by 3
PowerSeries.coeff_X_pow_mulproof · cited by 3
Polynomial.coe_mulproof · cited by 3
sum_range_powproof · cited by 2
PowerSeries.coeff_mul_X_powproof · cited by 2
PowerSeries.coeff_mul_X_pow'proof · cited by 2
PowerSeries.IsWeierstrassDivision.isUnit_of_map_ne_zeroproof · cited by 2
PowerSeries.order_mulproof · cited by 2