Skip to content

Generalise eq_fbig, eq_fbigl, eq_fbigr from Monoid.com_law to Monoid.law - #158

Open
pi8027 wants to merge 2 commits into
masterfrom
bigop-lemmas-without-commutativity
Open

pi8027 wants to merge 2 commits into
masterfrom
bigop-lemmas-without-commutativity

Conversation

@pi8027

@pi8027 pi8027 commented Nov 9, 2026

Copy link
Copy Markdown
Member

No description provided.

@pi8027
pi8027 force-pushed the bigop-lemmas-without-commutativity branch from ab288bd to 67f8339 Compare November 9, 2026 15:39
@pi8027

pi8027 commented Nov 9, 2026

Copy link
Copy Markdown
Member Author

I relaxed the commutativity assumption of other lemmas in BigComFSet since I need it for math-comp/multinomials#116. I'm unsure if it's worth backporting to finmap, though: https://github.com/math-comp/multinomials/blob/8d4896e54c256e012a1bac79f32992717a44674b/src/xfinmap.v#L71-L210

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant