feat(Foundations/Relation/Confluence): generalize results from confluence to commutation - #880

Merged

thomaskwaring merged 18 commits into

leanprover:mainfrom

thomaskwaring:comm-to-conf

Sep 13, 2026

Commits on Sep 7, 2026

basic results
twwar
committed
189476f
generalise to commutation
twwar
committed
fe95f37
docs
twwar
committed
bb51be0
fix build
twwar
committed
fb5b9e5
un-use deprecated theorems
twwar
committed
277a87b
lint
twwar
committed
f0fb93c

Commits on Sep 11, 2026

upstreaming note
twwar
committed
ffad88e
join2 naming
twwar
committed
e1c1009
grind annotations
twwar
committed
5b91545
scope grinds
twwar
committed
5be08e0

Commits on Sep 12, 2026

review comments
twwar
committed
5208f08
typeChanged annotations
twwar
committed
b7473e1
deprecate MJoin
twwar
committed
4716f0d
generalise DiamondCommute.extend
twwar
committed
2c8f99f
fix build combinatory logic
twwar
committed
59f9b05
further cleanup
twwar
committed
0e5cb48

Commits on Sep 13, 2026

remove MJoin2
twwar
committed
cff8880
symmetrise
twwar
committed
cfb0913