Theorem Submodule.toAddSubgroup_toAddSubmonoid

Modification history

2025-12-11 08:08
Mathlib/Algebra/Module/Submodule/Basic.lean
feat(RingTheory/Perfectoid): Fontaine's theta map is surjective (#26384) …
Added Submodule.toAddSubgroup_toAddSubmonoidView on Github →