METATHEOREM: Determine all laws implied by the abelian group of exponent 2 law 1571

[teorth]

It is shown in Theorem 4.6 that 1571 is indeed equivalent to being an abelian group of exponent 2. This should then imply a specific list of additional laws, which we could enumerate and prove in Lean.

The expected products here would be a metatheorem in Section 7, and a new file of all the implications (and anti-implications) with 1571 as hypothesis.

[teorth]

According to https://nicholas.carlini.com/tmp/view.html , there are 579 implications outstanding of this type.

[franklindyer]

claim

[teorth]

The automated prover component of this project has advanced so far that https://teorth.github.io/equational_theories/implications/?1571 now reports all implications in and out of this law have been classified. But it would still be good as a "unit test" to ensure that the theoretical implications from 1571 match what the automated provers are reporting.

[franklindyer]

propose PR #341

This PR has a general-purpose routine that is (hopefully) capable of resolving any consequence of Equation1571. It uses some bookkeeping involving free semigroups that is also included in the PR. Still working on the non-implications :-)

Since the consequences of Equation1571 have already been resolved, you can decide whether or not you want to include my changes. (There is a lot of bloat that went into building the general prover.) If not, just let me know and I'll withdraw the PR.

[teorth]

I think this is worth having in the Lean codebase - free abelian groups of order 2 are an intrinsically common object mathematically, and it is good to have some generalizable human-readable proofs in addition to the autogenerated ones which are often less insightful. It didn't pass CI though.