Can I use Lean 4 to construct operations via groups, ring...

Stream: lean4

[Kaje]

Can I use Lean4 to construct groups and fields and thus construct addition, subtraction, etc. on them? Basically the way I mean like is: Construct a group with the group axioms, then define operations that are bound to the group and lets you do operations on them.

[Henrik Böving]

Of course you can, docs4#Group to the rescue