Commit 2023-12-13 09:43 82ddb54f

chore: Sink Algebra.Support down the import tree (#8919) Function.support is a very basic definition. Nevertheless, it is a pretty heavy import because it imports most objects a support lemma can be written about. This PR reverses the dependencies between those objects and Function.support, so that the latter can become a much more lightweight import. Only two import could not easily be reversed, namely the ones to Data.Set.Finite and Order.ConditionallyCompleteLattice.Basic, so I created two new files instead. I credit:

• Yury for https://github.com/leanprover-community/mathlib/pull/6791
• Oliver for https://github.com/leanprover-community/mathlib/pull/7439