power series

Stream: general

[Kenny Lau]

import data.list.basic

universes u v

def power_series (α : Type u) : Type u :=
ℕ → α

variables {α : Type u}

instance [has_add α] : has_add (power_series α) :=
⟨λ x y n, x n + y n⟩

instance [has_zero α] [has_add α] [has_mul α] : has_mul (power_series α) :=
⟨λ x y n, list.sum $ (list.range (n+1)).map $ λ i, x i * y (n-i)⟩

[Kenny Lau]

Does anyone want to develop power series?

[Patrick Massot]

you

[Scott Morrison]

I wonder if we should invest some effort into listing new directions like this, perhaps with some commentary on difficulty and expected hurdles, and perhaps even with some suggestions about design, for the sake of new people coming to Lean (including students).

[Scott Morrison]

Particularly, some developments involve hard design decisions, and some don't so much. It would be good if the Kenny's of the world can focus their attention on the hard stuff, and we have a more explicit mechanism to hand out "straightforward" projects to relative beginners.

[Scott Morrison]

But maybe this is solving a problem that doesn't exist.

[Kevin Buzzard]

Kenny, post this on the IC chat as a possible project. Remind the students that they will be able to get a PR to mathlib under their belt if they take it on, and manage it. It might get done that way.

[Kevin Buzzard]

We can talk about it at Xena tonight.

[Scott Morrison]

Haha, I just posted on the ANU chat. :-)

[Kevin Buzzard]

This is exactly what these little chats are for.

[Kevin Buzzard]

If you guys do it then great. If we both do it then we end up writing some amalgamation, or taking what works best.

[Kevin Buzzard]

Beginner students are not scared to ask questions on those chats