mathlib

2bbc7e38 - feat(algebra/algebra/operations): the semiring of submodules over an algebra is idempotent (#18400)

feat(algebra/algebra/operations): the semiring of submodules over an algebra is idempotent (#18400) The same results are repeated for `ideal`. The two modifications of ported files are docstrings only, and are forward-ported at https://github.com/leanprover-community/mathlib4/pull/2175. Since this adjusts the import hierarchy slightly, there are some files which now need to qualify names that were previously unambiguous. One proof timed out, but the timeout went away after converting a messy term into tactic mode.