Commit 2024-11-11 13:54 b407af36

chore(Algebra/Field): split Subfield.lean into Defs and Basic (#18528) This PR splits off a Defs.lean file from Subfield.lean containing on the definition and field structure of Subfield(Class). This PR was motivated by the "hoard factor" computation that showed https://github.com/leanprover-community/mathlib4/pull/18520 increased the factor of Mathlib.Algebra.Order.Field.Subfield by a lot, meaning there are many transitive imports in that file whose declarations remain unused. The previous PR increased it from 0,814203 to 0,828997, this PR reduces it down to 0,784072