Viewing profile — hutchisonc

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 al…

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 …

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

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.