hutchisonc

vor 4 Jahrendiscuss

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 prove the independence of the continuum hypothesis from ZFC in Lean; see https://github.com/flypitch/flypitch.

hutchisonc

vor 4 Jahrendiscuss

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 elliptic curves, it turns out there is a bijection between the complex points on the curve and the elements of (the degree 0 subgroup of) its Picard group, so it inherits the group structure this way. This is the same group structure as the usual one defined explicitly. I might write more about this when I get home.

hutchisonc

vor 5 Jahrendiscuss

+1. The lemma is trivial not because the result isn't deep but because we have the right definitions.

hutchisonc

vor 5 Jahrendiscuss

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.

comments