Commit 2024-10-24 15:01 03be9898

chore(Algebra/Module): split Defs a bit further (#18169) There are quite a few imports in Module/Defs.lean that are not needed for defining modules. So this PR rearranges the results in the file to postpone those imports. Changes:

• The result involving Invertible go to Module/Basic.lean
• The results involving AddMonoid.End goes to the new file Module/End.lean
• The results involving Opposite go to the new file Module/Opposite.lean; the previous Module/Opposites.lean is now Module/Equiv/Opposite.lean (note: now in singular to match the other Opposite file)