Can I do the group theory related theorem proving, say, Rearrangement
Theorem [1], by coq?
[1] https://mathworld.wolfram.com/RearrangementTheorem.html
Regards
HZ
if you're content with finite groups, I'd recommend looking at the encoding of finite groups in MathComp, in particular fingroup.v. See also the math-comp users stream
Last updated: Mar 29 2024 at 13:01 UTC