search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
Apache License 2.0
78 stars 19 forks source link

SUBGRAPH: Show 40 does not imply 3, 8, 42, 43, 4512; and 4, 387, 4582 does not imply 40 #31

Open teorth opened 5 hours ago

teorth commented 5 hours ago

Only a generating set of implications needs to be added to Subgraph.lean, of course. Human-readable sketches of proofs can be added in comments.

teorth commented 2 hours ago

Added Seraphina Nix's sketch of proofs (from https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Outstanding.20tasks.2C.20v1/near/473000267) in the comments.