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):

https://www.githubstatus.com/

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