identities

Stream: general

[Bryan Gin-ge Chen]

I'm thinking about PRing a new file algebra/group_power/identities.lean with a number of identities that are all provable by ring, e.g.:

• Sophie Germain's identity, see the comments by @Joseph Myers in the comments of #4261
• Brahmagupta-Fibonacci (sum of two squares) and some generalizations
• Euler's sum of four squares (this is currently taken care of by ring in Chris Hughes's proof of Lagrange's Four Square Theorem),
• Degen's sum of eight squares, (the profiler says ring takes 252 ms to prove this)

I was motivated by the discussion in #4261 linked above and the related thought that people may end up searching for "named" identities like these. On the other hand, the ring tactic is probably easier to use in any real applications these might have, especially since there are tons of slight variations coming from choices of sign, permutations, etc.

Does anyone have any strong opinions?

[Scott Morrison]

Seems reasonable. We could maybe even think of these examples as part of the documentation of ring.

[Scott Morrison]

(That is, they are 100% appropriate in test/ring.lean or similar. I'm happy with them in src/, as well.)

[Scott Morrison]

I guess they could also be a file under tutorials ---- a file that explains what ring does through interesting examples.)

[Bryan Gin-ge Chen]

I was thinking of putting the file in src/ so that I could replace the ring invocations in the IMO file added in #4261 and number_theory/sum_four_squares, but maybe that just adds an unnecessary dependency.

[Bryan Gin-ge Chen]

@Scott Morrison Is the :+1: for replacing the ring calls or that doing so would be unnecessary?

[Bryan Gin-ge Chen]

Or both? :smiley:

[Johan Commelin]

@Bryan Gin-ge Chen I like your suggestion. Making sum_four_squares even epsilon more readable is a good enough reason to put these things in src/

[Bryan Gin-ge Chen]

I opened #4390.