Skip to content

feat: Add DropPair ProdP commutation lemma for one orientation - #1345

Open
NicolaBernini wants to merge 8 commits into
leanprover-community:masterfrom
NicolaBernini:feat/add-DropPair-ProdP-commutation-lemmas-for-one-orientation-1July2026
Open

feat: Add DropPair ProdP commutation lemma for one orientation#1345
NicolaBernini wants to merge 8 commits into
leanprover-community:masterfrom
NicolaBernini:feat/add-DropPair-ProdP-commutation-lemmas-for-one-orientation-1July2026

fix: drop fragile left-factor dropPair commutation

30cf76f
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Python based style linter
succeeded Jul 3, 2026 in 17s