refactor(analysis/normed_space/basic): add semi_normed_ring (#6889)

This is the natural continuation of #6888 . We add here semi_normed_ring, semi_normed_comm_ring, semi_normed_space and semi_normed_algebra. I didn't add `semi_normed_field`: the most important result for normed_field is `∥1∥ = 1`, that is false for `semi_normed_field`, making it a more or less useless notion. In particular a `semi_normed_space` is by definition a vector space over a `normed_field`.
leanprover-community · Mar 31, 2021 · 1fdce2f · 1fdce2f
1 parent 85c8961
commit 1fdce2f
Show file tree

Hide file tree

Showing 3 changed files with 225 additions and 94 deletions.
diff --git a/docs/overview.yaml b/docs/overview.yaml
@@ -230,7 +230,7 @@ Topology:
 Analysis:
   Normed vector spaces:
     normed vector space over a normed field: 'normed_space'
-    topology on a normed vector space: 'normed_space.has_continuous_smul'
+    topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
     finite dimensional normed spaces over complete normed fields are complete: 'submodule.complete_of_finite_dimensional'
     Heine-Borel theorem (finite dimensional normed spaces are proper): 'finite_dimensional.proper'

diff --git a/docs/undergrad.yaml b/docs/undergrad.yaml
@@ -412,7 +412,7 @@ Topology:
     complete metric spaces: 'metric.complete_of_cauchy_seq_tendsto'
     contraction mapping theorem: 'contracting_with.exists_fixed_point'
   Normed vector spaces on $\R$ and $\C$:
-    topology on a normed vector space: 'normed_space.has_continuous_smul'
+    topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
     equivalent norms:
     Banach open mapping theorem: 'open_mapping'
     equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'