Zulip Chat Archive

Stream: maths

Topic: rings and ideals


view this post on Zulip Patrick Massot (Jul 21 2018 at 11:34):

@Kenny Lau and @Chris Hughes with the recent merge of PR196 how does current mathlib compare to Lean 2 lib?

view this post on Zulip Chris Hughes (Jul 21 2018 at 17:56):

Is that a hint that I should work on ideals? I was delayed by type class problems, but now I've found a long term solution, so I can work on it properly.

view this post on Zulip Mario Carneiro (Jul 21 2018 at 17:59):

was the lean 2 ideals library significant?

view this post on Zulip Chris Hughes (Jul 21 2018 at 18:02):

Looking at it, although it's much longer than the ideals file in mathlib, a lot of it covers stuff that's already done for modules.

view this post on Zulip Mario Carneiro (Jul 21 2018 at 18:03):

aren't those easy then? I thought mathlib ideals were defined in terms of submodules, so it should just be a theorem application away

view this post on Zulip Chris Hughes (Jul 21 2018 at 18:03):

Exactly.

view this post on Zulip Chris Hughes (Jul 21 2018 at 18:03):

Is it even worth proving them specifically for ideals?

view this post on Zulip Mario Carneiro (Jul 21 2018 at 18:04):

It can be helpful to change the statement the way you need it, if it is going to be used in rw for example

view this post on Zulip Mario Carneiro (Jul 21 2018 at 18:05):

I have said before that the most important thing about many of the early files is the statements, not the proofs


Last updated: May 06 2021 at 18:20 UTC