Commit 2023-11-01 13:33 b5013c29

View on Github →

feat: compute Monoid.exponent as the lcm over pi types and Prod (#8066)

Estimated changes

Modified Mathlib/GroupTheory/Exponent.lean

added theorem Monoid.exponent_pi

added theorem Monoid.exponent_pi_eq_zero

added theorem Monoid.exponent_prod

added theorem MonoidHom.exponent_dvd