Commit 2024-04-19 13:15 46c2efe1

chore: small splits of RingTheory.Ideal.Operations; clean imports (#12090) This is based on seeing the import RingTheory.Ideal.Operations → LinearAlgebra.Basis on the longest pole. It feels like Ideal.Operations is a bit of a chokepoint for compiling Mathlib since it imports many files and is imported by many files. So splitting out a few obvious parts should help with compile times. Moreover, there are a bunch of imports that I could remove and have the file still compile: presumably these are (were) transitive dependencies that shake does not remove. The following results and their corollaries were split off:

• Ideal.basisSpanSingleton
• Basis.mem_ideal_iff
• Ideal.colon In particular, now Ideal.Operations should no longer need to know about Basis or submodule quotients.