hutchisonc

4 ms·

1. 1.▲
   by hutchisonc 4y ago

   The mathlib discussed in the article does include representations of infinite cardinalities; see e.g. https://leanprover-community.github.io/mathlib_docs/data/rea... . There was also a (now completed) project to pr
2. 2.▲
   by hutchisonc 4y ago

   For what it’s worth, in the math context (not thinking about applications), the group law is extremely natural. Every variety has an associated group called the Picard group tells you something about geometry of the variety. But for ellipti
3. 3.▲
   by hutchisonc 6y ago

   +1. The lemma is trivial not because the result isn't deep but because we have the right definitions.
4. 4.▲
   by hutchisonc 6y ago

   Many of the commenters here need to learn how to take a few deep breaths and not take it so seriously. Not everyone is going to communicate the way you want and that’s fine.