Zulip Chat Archive
Stream: general
Topic: zsqrtd.nonsquare in number_theory/pell
Kenny Lau (May 27 2018 at 11:58):
This should be a Prop @Mario Carneiro
Kevin Buzzard (May 27 2018 at 11:59):
Submit a PR
Kenny Lau (May 27 2018 at 14:25):
@Mario Carneiro will you fix it yourself, or should I submit a PR?
Kenny Lau (May 27 2018 at 14:25):
(I might also prove that it is decidable)
Mario Carneiro (May 27 2018 at 14:26):
I fixed it, decidability is a bit weird since it's a typeclass
Kenny Lau (May 27 2018 at 14:26):
it's also a proposition
Last updated: Dec 20 2023 at 11:08 UTC