PR !4#11575: feat(RingTheory/HahnSeries/Addition): lemmas...

Stream: triage

[Random Issue Bot]

Today I chose PR #11575 for discussion!

feat(RingTheory/HahnSeries/Addition): lemmas on leading terms
Created by @Scott Carnahan (@ScottCarnahan) on 2024-03-22
Labels: WIP, merge-conflict, t-ring-theory

Is this PR still relevant? Any recent updates? Anyone making progress?

[Scott Carnahan]

The material here was not as useful as I had hoped. I will close it.