feat: Port `algebra/monoid.v` and `algebra/big_op.v` - #132

Merged

lzy0505 merged 14 commits into

leanprover-community:masterfrom

lzy0505:zliu/algebra-bigop-monoid

Mar 16, 2026

Commits on Mar 2, 2026

feat: Add BigOp algebra and monoid definitions
lzy0505
committed
7b97935

Commits on Mar 4, 2026

Clean up
lzy0505
committed
0ca2cac
Update PORTING.md
lzy0505
committed
d8215c1

Commits on Mar 5, 2026

Add notations
lzy0505
committed
fd9c653

Commits on Mar 10, 2026

chore: cleanup monoid
markusdemedeiros
committed
8293356
chore: cleanup bigOpL (checkpoint)
markusdemedeiros
committed
a553080

Commits on Mar 12, 2026

chore: cleanup names (checkpoint)
markusdemedeiros
committed
d477833
checkpoint
markusdemedeiros
committed
a939d90

Commits on Mar 13, 2026

checkpoint
markusdemedeiros
committed
40c62c1
more refactoring
markusdemedeiros
committed
1ee12f9

Commits on Mar 14, 2026

chore: cleanup
markusdemedeiros
committed
4387347

Commits on Mar 16, 2026

chore: cleanup pass
markusdemedeiros
committed
a5611b7
chore: cleanup
markusdemedeiros
committed
1d703ed
Merge branch 'master' into zliu/algebra-bigop-monoid
markusdemedeiros
authored
5bc41cc