Theorems · Theorem · commutative algebra

LaurentSeries.hasseDeriv_single_add

∀ {R : Type u_1} [inst : Semiring R] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module R V] (k : ℕ) (n : ℤ)
  (x : V),
  (LaurentSeries.hasseDeriv R k) ((HahnSeries.single (n + ↑k)) x) = (HahnSeries.single n) (Ring.choose (n + ↑k) k • x)

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommGroupModule