Filtered Algebra

Stream: PR reviews

[Nailin Guan]

Hello, we have opened a series of PR for filtered ring/algebra/module, the associated graded structure and some basic things about their exactness. Previously there is #20900 merged. The dependencies between the incoming ones are as follow:
4d5e2c0a5c489cc5372c01992c3618c.jpg

[Eric Wieser]

A -> B means "A needs B to be merged first" (A depends on B) or "A is the pre-work for B" (B depends on A)?

[Nailin Guan]

Yes, sorry that I didn't make it clear.

[Eric Wieser]

Which meaning did you intend?

[Kevin Buzzard]

aka "where do we start?" (answer: A -> B in the diagram seems to mean "B depends on A")

[Nailin Guan]

A->B mean B depend on A, we can start at #22631
#PR reviews > #22631 define associated graded structure for abelian group
There is another PR with no dependency at #22705 consisting of only some relevant lemma

[Nailin Guan]

Currently, #22705 is merged.
Can anybody have more look on #22631? Thanks