Split analysis.normed_space.basic

Stream: general

[Yury G. Kudryashov]

Hi, it looks to me that src#analysis.normed_space.basic is a huge with a few (related) topics mixed together. I'm moving (semi_)normed_group to a separate file in #9642. I plan to further split it into normed.ring, normed.field, normed.space (or normed.module because I think that we should generalize to normed modules over normed rings), and normed.algebra.

[Yury G. Kudryashov]

Any objections?

[Yaël Dillies]

The bot should really support filenames... Does src#analysis/convex/basic work?

[Yaël Dillies]

Nope

[Yaël Dillies]

Do you plan on migrating the rest of analysis.normed_space. to analysis.normed.? I think that's justified. Or at least move it to analysis.normed.space.

[Yaël Dillies]

The file splits seem to align on what we already have in other hierarchies, so I'm all for it.

[Yaël Dillies]

Feel free to expand the docstrings as you go along.

[Yury G. Kudryashov]

I want to make the "split file" PRs atomic, so I'll review code / docstrings / var names in separate PRs.

[Yaël Dillies]

Yeah sure! I didn't obviously mean in the same PR.

[Yury G. Kudryashov]

It would be nice if someone approves or rejects #9642.

[Yury G. Kudryashov]

It is +1K,-1K but actually there is no new code here (I even resisted the temptation to rename vars in the same commit).