Zulip Chat Archive

Stream: general

Topic: power series


view this post on Zulip 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}

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)

view this post on Zulip Kenny Lau (Mar 07 2019 at 10:06):

Does anyone want to develop power series?

view this post on Zulip Patrick Massot (Mar 07 2019 at 10:07):

you

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Mar 07 2019 at 10:51):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:07):

We can talk about it at Xena tonight.

view this post on Zulip Scott Morrison (Mar 07 2019 at 11:08):

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

view this post on Zulip Kevin Buzzard (Mar 07 2019 at 11:08):

This is exactly what these little chats are for.

view this post on Zulip 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.

view this post on Zulip 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