Open teorth opened 2 weeks ago
Proof is in https://teorth.github.io/equational_theories/blueprint/1516-chapter.html .
Proof can go in the ManuallyProven folder. When done, update ManuallyProved.lean, place \lean and \leanok tags as appropriate in the blueprint, and remove the appropriate conjecture from Conjectures.lean.
ManuallyProven
ManuallyProved.lean
Conjectures.lean
Proof is in https://teorth.github.io/equational_theories/blueprint/1516-chapter.html .
Proof can go in the
ManuallyProvenfolder. When done, updateManuallyProved.lean, place \lean and \leanok tags as appropriate in the blueprint, and remove the appropriate conjecture fromConjectures.lean.