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: Prove 5 does not imply 42, 43, 4513 #32

Open teorth opened 6 hours ago

teorth commented 6 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

Seraphina Nix's sketch of proof (from https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Outstanding.20tasks.2C.20v1/near/472989978) is included in the comments to the Lean file.

ChienYungChi commented 1 hour ago

claim