Mathlib Changelog
v4
Changelog
About
Github
Def
AddCommMonoid.zmodModule
Modification history
2024-05-07 01:05
Mathlib/Data/ZMod/Module.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted
AddCommMonoid.zmodModule
View on Github →
2023-12-26 04:50
Mathlib/Data/ZMod/Module.lean
feat: `AddCommGroup` is `ZMod n` module if `n • x = 0` for all `x` (#9017) …
Added
AddCommMonoid.zmodModule
View on Github →