Commit 2024-11-05 11:39 f4eec872

chore(Algebra/Ring/Subring): split Basic.lean (#18520) This PR splits off a Defs.lean file from Subring/Basic.lean containing on the definition and subsemiring structure of Subring(Class). This PR was motivated by the "hoard factor" computation that showed #18340 increased the factor of Algebra.Ring.Action.Invariant by a lot, meaning there are many transitive imports in that file whose declarations remain unused. The old PR increased it from 0,838219 to 0,859692, this PR decreases it back to 0,821529. Unfortunately, Mathlib's overall hoard factor increased somewhat, from 0,624155 to 0,624658. The solution might be to split files higher up in the hierarchy?