Zulip Chat Archive
Stream: maths
Topic: is_projective
Riccardo Brasca (Jun 07 2021 at 09:36):
Is there a reason why docs#is_projective is a def and not a class?
Kevin Buzzard (Jun 07 2021 at 09:39):
Is it something to do with Lean 4 porting or something like that?? Maybe in Lean 4 defs can't be classes??
Kevin Buzzard (Jun 07 2021 at 09:43):
OK looking at doc blame I have a new conjecture: I wrote this and I should have made it a class but I didn't, and somehow it got past the PR process. That's another possibility.
Riccardo Brasca (Jun 07 2021 at 09:45):
:grinning: I will refactor this
Eric Wieser (Jun 07 2021 at 10:50):
It's probably not a class yet because there's only one lemma that would use it (docs#is_projective.lifting_property), and nothing uses that yet
Riccardo Brasca (Jun 07 2021 at 10:52):
Last updated: Dec 20 2023 at 11:08 UTC