Theorem Monoid.exponent_prod

Modification history

2023-11-01 13:33
Mathlib/GroupTheory/Exponent.lean
feat: compute `Monoid.exponent` as the lcm over pi types and `Prod` (#8066)
Added Monoid.exponent_prodView on Github →