Commit 2025-02-28 22:16 38115a55

chore(Data/Set): avoid importing algebra in Data/Set/Countable.lean (#21874) By splitting off Encodable instances for vectors / Pi types, we can avoid importing Monoid in Data/Set/Countable.lean. An alternative approach is to redo the proofs in Logic.Encodable.Pi to reduce the dependencies. Looking at the dependency graph for MeasureTheory.MeasureSpace.Defs this whole swath of files is unused, so we might as well move them out to skip them all.