Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-09-29 20:51
d4f0e62a
View on Github →
feat:
x ∈ toZModSubmodule n S ↔ x ∈ S
(
#17210
) From LeanAPAP
Estimated changes
Modified
Mathlib/Data/ZMod/Module.lean
modified
theorem
AddSubgroup.coe_toZModSubmodule
added
theorem
AddSubgroup.mem_toZModSubmodule