Zulip Chat Archive

Stream: maths

Topic: rings and ideals

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?

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.

Mario Carneiro (Jul 21 2018 at 17:59):

was the lean 2 ideals library significant?

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.

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

Chris Hughes (Jul 21 2018 at 18:03):

Exactly.

Chris Hughes (Jul 21 2018 at 18:03):

Is it even worth proving them specifically for ideals?

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

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: Dec 20 2023 at 11:08 UTC