Commit 2025-03-09 23:03 63a7be57

refactor(Mathlib/Analysis/Normed): disentangle normed rings and normed fields (#22744) This PR moves around a bunch of code in the directories Normed/Ring and Normed/Field in order to make sure that everything that involves NormedField or NormedDivisionRing is in the Field subdirectory, and everything which doesn't require inverses is in Ring. I also moved the files for "unbundled" norms / seminorms into a separate directory, because I couldn't find a good place for them otherwise – the problem is that several of them prove results about ring (semi)norms, but require results about the real numbers that depend on normed-field theory.