Commit 2025-03-17 13:17 4eedae49

chore(Algebra/Algebra): reorganize Algebra.adjoin and complete lattice (#22557) This PR creates a new file that holds the definition and basic results on Algebra.adjoin and the resulting CompleteLattice (Subalgebra R A) instance, moving definitions downstream from Subalgebra/Basic.lean and some lemmas upstream from RingTheory/Adjoin/Basic.lean. A nice consequence is that we can avoid importing linear algebra (in the form of Basis) in quite a few measure theory files. (In fact we should be able to do a bit better and avoid Algebra altogether, but that's for later PRs.)