Theorem AddSubgroup.mem_toZModSubmodule

Modification history

2024-09-29 20:51
Mathlib/Data/ZMod/Module.lean
feat: `x ∈ toZModSubmodule n S ↔ x ∈ S` (#17210) …
Added AddSubgroup.mem_toZModSubmoduleView on Github →