Zulip Chat Archive
Stream: general
Topic: nat.mul_le_mul
Kevin Buzzard (Jun 29 2020 at 10:08):
Is it intentional that nat.mul_le_mul asks twice for proofs that 0 <= (n : nat)? Is this for some general consistency with mul_le_mul lemmas? I thought the whole point of namespaced lemmas like that was precisely so you could change the inputs appropriately.
Johan Commelin (Jun 29 2020 at 10:09):
I guess it is not.
Johan Commelin (Jun 29 2020 at 10:10):
Probably an artifact from me reproving a bunch of lemmas specifically for nat when ripping algebra out of core.
Johan Commelin (Jun 29 2020 at 10:10):
I guess this is in core?
Bryan Gin-ge Chen (Jun 29 2020 at 10:10):
Yep: src#nat.mul_le_mul
Johan Commelin (Jun 29 2020 at 10:12):
Surrounding lemmas have the same problem.
Johan Commelin (Jun 29 2020 at 10:19):
I'm trying to fix this, but lean spits out loads of unrelated errors...
Johan Commelin (Jun 29 2020 at 10:20):
Is github down for everyone or just me?
Kevin Buzzard (Jun 29 2020 at 10:20):
maybe everyone?
Shing Tak Lam (Jun 29 2020 at 10:21):
Everyone
Johan Commelin (Jun 29 2020 at 10:21):
Stupid github
Kevin Buzzard (Jun 29 2020 at 10:21):
back now but slow
Johan Commelin (Jun 29 2020 at 10:23):
https://github.com/leanprover-community/lean/compare/fix-nat-lemmas?expand=1
Last updated: Dec 20 2023 at 11:08 UTC