Theorem Submodule.toAddSubmonoid_sSup

Modification history

2024-01-16 21:01
Mathlib/Algebra/Module/Submodule/Lattice.lean
feat: basic theory connecting `R[X]`-submodules and invariant `R`-submodules (#9721)
Added Submodule.toAddSubmonoid_sSupView on Github →