Commit 2025-09-22 11:55 baf3075a

chore(Algebra/Category/Grp): don't import AddCircle in Injective.lean (#29811) The file Grp/Injective.lean contained an injectivity result for AddCircle, but this is immediately derived from existing instances. It used to have a much more complex proof. Since AddCircle brings with it a whole bunch of analysis and topology imports that we don't need for this algebraic theory, this saves us a couple hundred transitive imports. Also, clean up the module docs to reflect the current situation. I have moved the instance to a test file, to ensure it remains accessible even after future refactors. This import was spotted in the same PR run as #29808, but does not change the top-level directory import structure in the same way.