Zulip Chat Archive

Stream: general

Topic: identities

Bryan Gin-ge Chen (Oct 03 2020 at 00:33):

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.:

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 (Oct 03 2020 at 01:17):

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

Scott Morrison (Oct 03 2020 at 01:18):

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

Scott Morrison (Oct 03 2020 at 01:19):

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

Bryan Gin-ge Chen (Oct 03 2020 at 01:25):

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 (Oct 03 2020 at 01:34):

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

Bryan Gin-ge Chen (Oct 03 2020 at 01:34):

Or both? :smiley:

Johan Commelin (Oct 03 2020 at 04:09):

@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 (Oct 04 2020 at 00:41):

I opened #4390.

Last updated: Aug 03 2023 at 10:10 UTC