def LaurentSeries.residue (k : Type u_1) [Field k] : LaurentSeries k →ₗ[k] k

The residue k-linear map on Laurent series: extracting the coefficient of t^{-1}, the algebraic incarnation of the analytic residue at the origin.

@[simp]

theorem LaurentSeries.residue_apply {k : Type u_1} [Field k] (f : LaurentSeries k) : (residue k) f = f.coeff (-1)

Unfolding lemma: the residue of f is the coefficient of t^{-1}.

@[simp]

theorem LaurentSeries.residue_single_neg_one {k : Type u_1} [Field k] (a : k) : (residue k) ((HahnSeries.single (-1)) a) = a

The residue of a · t^{-1} is a (residue of a pure principal monomial).

theorem LaurentSeries.residue_single_of_ne {k : Type u_1} [Field k] {n : ℤ} (h : n ≠ -1) (a : k) : (residue k) ((HahnSeries.single n) a) = 0

The residue of a · t^n for n ≠ -1 is zero.

@[simp]

theorem LaurentSeries.residue_zero {k : Type u_1} [Field k] : (residue k) 0 = 0

The residue map sends the zero Laurent series to zero.

theorem LaurentSeries.residue_add {k : Type u_1} [Field k] (f g : LaurentSeries k) : (residue k) (f + g) = (residue k) f + (residue k) g

Additivity of the residue map.

theorem LaurentSeries.residue_smul {k : Type u_1} [Field k] (c : k) (f : LaurentSeries k) : (residue k) (c • f) = c • (residue k) f

k-linearity (scalar compatibility) of the residue map.

@[simp]

theorem LaurentSeries.residue_ofPowerSeries {k : Type u_1} [Field k] (f : PowerSeries k) : (residue k) ((HahnSeries.ofPowerSeries ℤ k) f) = 0

The residue of an honest power series (no principal part) is zero.

theorem LaurentSeries.residue_uniformizer_inv {k : Type u_1} [Field k] : (residue k) ((HahnSeries.single (-1)) 1) = 1

Normalization: the residue of 1 · t^{-1} is 1, the canonical generator.