Mathlib.Algebra.Associated

Stream: mathlib4

[Kim Morrison]

Mathlib.Algebra.Associated looks like it could do with a split.

[Yaël Dillies]

Agreed, will do it soon

[Ruben Van de Velde]

I've got #7200 open which Yaël didn't like, and I started on https://github.com/leanprover-community/mathlib4/compare/split-associated-irreducible-prime?expand=1 but lost track at some point

[Yaël Dillies]

Actually #9411 happened since you wrote #7200, so maybe you could try splitting again

[Yaël Dillies]

#11863 removes a bunch of algebraic order dependencies to Algebra.Associated

[Yaël Dillies]

The rest will disappear if we move Associates to its own file (which sounds reasonable?)