local_ring): split file (#17319)

Commit

3 years ago

chore(ring_theory/ideal/local_ring): split file (#17319) This way large parts of `analysis` no longer depend on `category_theory`.

Author

urkud

Parents