Theorem MonoidHom.exponent_dvd

Modification history

2024-02-05 18:00
Mathlib/GroupTheory/Exponent.lean
refactor(Data/FunLike): use unbundled inheritance from FunLike (#8386) …
Modified MonoidHom.exponent_dvdView on Github →
2023-11-01 13:33
Mathlib/GroupTheory/Exponent.lean
feat: compute `Monoid.exponent` as the lcm over pi types and `Prod` (#8066)
Added MonoidHom.exponent_dvdView on Github →