feat: Port algebra/monoid.v and algebra/big_op.v

[lzy0505]

Description

Part of #113

• ported algebra/monoid.v
• ported big_opL and big_opM parts of algebra/big_op.v

Proofs for some map lemmas are longer than those for their Rocq counterparts because we’re working with generic finite maps while Rocq only uses gmap.

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[lzy0505]

I've rebased this PR to use the new FiniteMap API. Can you have a look? @markusdemedeiros
I tried to avoid using ExtensionalPartialMap, which makes some proofs a bit annoying.

[markusdemedeiros]

Ok, I'm done! Look over my changes and merge when you are ready.

[lzy0505]

Thanks for cleaning up! Looks good to me. Merging now.