## Stream: general

### Topic: power series

#### Kenny Lau (Mar 07 2019 at 10:06):

import data.list.basic

universes u v

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

variables {α : Type u}

⟨λ 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 (Mar 07 2019 at 10:06):

Does anyone want to develop power series?

you

#### Scott Morrison (Mar 07 2019 at 10:49):

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 (Mar 07 2019 at 10:51):

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 (Mar 07 2019 at 10:51):

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

#### Kevin Buzzard (Mar 07 2019 at 11:07):

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 (Mar 07 2019 at 11:07):

We can talk about it at Xena tonight.

#### Scott Morrison (Mar 07 2019 at 11:08):

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

#### Kevin Buzzard (Mar 07 2019 at 11:08):

This is exactly what these little chats are for.

#### Kevin Buzzard (Mar 07 2019 at 11:08):

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 (Mar 07 2019 at 11:08):

Beginner students are not scared to ask questions on those chats

Last updated: May 14 2021 at 04:22 UTC