Theorems · Theorem · commutative algebra

PowerSeries.coeff_coe

∀ {R : Type u_1} [inst : Semiring R] (f : PowerSeries R) (i : ℤ),
  ((HahnSeries.ofPowerSeries ℤ R) f).coeff i = if i < 0 then 0 else (PowerSeries.coeff i.natAbs) f

Defined in

Mathlib.RingTheory.LaurentSeries

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring