CIRCLE WITH A DOT

@johncarlosbaez Another classic is of course 1/0 = 0 and its corollary, ζ(1) = (γ - log(4π))/2. https://leanprover-community.github.io/mathlib4_docs/Mathlib/NumberTheory/Harmonic/ZetaAsymp.html#riemannZeta_one

@johncarlosbaez There's a tactic/script that converts proofs of statements for groups to the corresponding statement for additive groups, but it's not yet seamless.

@johncarlosbaez No, it's an additive group, which is a distinct thing from a group (which happens to be defined in the same way but with different notation).

@johncarlosbaez "It forces you to think about mathematics in the right way." is such a rich statement given the amount of mathematical jank there is in Mathlib.

For example, did you know that (ℝ,+) is technically not a group?