building API for ratfunc and laurent series

Stream: new members

[Yakov Pechersky]

On branch#pechersky/laurent-expansion, I can state the following:

import field_theory.ratfunc

universes u v

variables {R : Type u} [field R]

open ratfunc power_series

@[simp] lemma mv_power_series.constant_coeff_mk {σ : Type v} {R : Type u} [semiring R]
  (f : (σ →₀ ℕ) → R) : mv_power_series.constant_coeff σ R f = f 0 := rfl

@[simp] lemma power_series.constant_coeff_mk {R : Type u} [semiring R] (f : ℕ → R) :
  power_series.constant_coeff R (power_series.mk f) = f 0 := rfl

example : ((X / (X - 1) : ratfunc R) : laurent_series R) =
  (mk (λ i, if i = 0 then (0 : R) else -1)) :=
begin
  have : ((polynomial.X - polynomial.C 1 : polynomial R) : laurent_series R) ≠ 0,
  { refine ne_of_apply_ne (λ x : laurent_series R, x.coeff 0) _,
    rw [coe_coe, power_series.coeff_coe],
    simp },
  rw [←algebra_map_X, ←map_one (@ratfunc.C R _ _), ←algebra_map_C, ←map_sub, coe_div,
      div_eq_iff this, coe_coe, coe_coe, ←coe_mul, sub_eq_add_neg, polynomial.coe_add,
      mul_add, polynomial.coe_X, ←map_neg, polynomial.coe_C],
  ext i,
  rw [coeff_coe, coeff_coe, map_add],
  induction i using int.induction_on with i IH i IH,
  { simp },
  { rw [int.coe_nat_add_one_out, int.nat_abs_of_nat, if_neg (int.coe_nat_succ_pos _).not_lt,
        if_neg (int.coe_nat_succ_pos _).not_lt, coeff_succ_mul_X, coeff_mul_C],
    simp [coeff_X, nat.succ_inj', ite_add] },
  { simp_rw [←int.neg_succ_of_nat_coe', if_pos (int.neg_succ_lt_zero i)] }
end

[Yakov Pechersky]

which is on the way to being able to neatly state the following claims:
image.png

[Yakov Pechersky]

Are there any suggestions over what API should be built to make this smoother?

[Adam Topaz]

Laurent series are a DVR and evaluation at 0 corresponds to the projection onto the residue field. We should probably build on the API that relates general nonsense stuff about DVRs to explicit formulas using Laurent series. (That's vague, I know...)