Commit 2022-01-16 13:30 02a4775a

refactor(analysis/normed_space): merge normed_space and semi_normed_space (#8218) There are no theorems which are true for [normed_group M] [normed_space R M] but not [normed_group M] [semi_normed_space R M]; so there is about as much value to the semi_normed_space / normed_space distinction as there was between module / semimodule. Since we eliminated semimodule, we should eliminte semi_normed_space too. This relaxes the typeclass arguments of normed_space to make it a drop-in replacement for semi_normed_space; or viewed another way, this removes normed_space and renames semi_normed_space to replace it. This does the same thing to normed_algebra and seminormed_algebra, but these are hardly used anyway. Zulip As with any typeclass refactor, this randomly breaks elaboration in a few places; presumably, it was able to unify arguments from one particular typeclass path, but not from another. To fix this, some type ascriptions have to be added where previously none were needed. In a few rare cases, the elaborator gets so confused that we have to enter tactic mode to produce a term. This isn't really a new problem - this PR just makes these issues all visible at once, whereas normally we'd only run into one or two at a time. Optimistically Lean 4 will fix all this, but we won't really know until we try.