[Merged by Bors] - feat(Algebra/Module/Submodule): Symmetric submodules are modular elements in the lattice of submodules over a semiring#36689

martinwintermath wants to merge 11 commits intoleanprover-community:masterleanprover-community/mathlib4:masterfrom

martinwintermath:submodule-modular-elementmartinwintermath/mathlib4:submodule-modular-elementCopy head branch name to clipboard