feat(Analysis/Normed): the SeminormedRing structure determined by a RingSeminorm (leanprover-community#38407)

Parallel to [RingNorm.toNormedRing](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Normed/Unbundled/RingSeminorm.html#RingNorm.toNormedRing), defines the `SeminormedRing` structure on a ring `R` determined by a `RingSeminorm`.

Author: mbkybky

Mathlib/Analysis/Normed/Unbundled/RingSeminorm.lean

@@ -153,6 +153,12 @@ theorem seminorm_one_eq_one_iff_ne_zero (hp : p 1 ≤ 1) : p 1 = 1 ↔ p ≠ 0 :
   · refine hp.antisymm ((le_mul_iff_one_le_left hp0).1 ?_)
     simpa only [one_mul] using map_mul_le_mul p (1 : R) _
 
+/-- The `SeminormedRing` structure on a ring `R` determined by a `RingSeminorm`. -/
+abbrev toSeminormedRing : SeminormedRing R where
+  __ := ‹Ring R›
+  __ := p.toAddGroupSeminorm.toSeminormedAddCommGroup
+  norm_mul_le := map_mul_le_mul p
+
 end Ring
 
 section CommRing
@@ -259,7 +265,7 @@ instance [DecidableEq R] : Inhabited (RingNorm R) :=
 
 end NonUnitalRing
 
-/-- The `NormedRing` structure on a ring `R` determined by a `RingNorm` -/
+/-- The `NormedRing` structure on a ring `R` determined by a `RingNorm`. -/
 -- See note |reducible non-instances]
 abbrev toNormedRing [Ring R] (f : RingNorm R) : NormedRing R where
   __ := ‹Ring R›