Theorem Monoid.exponent_pi

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_piView on Github →