English
If a nonunital normed ring E with a star operation satisfies the inequality ||x|| · ||x|| ≤ ||x x⋆|| for all x, then E can be endowed with a C*-ring structure.
Русский
Если неабстрагируемое нормированное кольцо E с операцией звезды удовлетворяет неравенству ||x|| · ||x|| ≤ ||x x⋆|| для всех x, то E можно наделить структурой C*-кольца.
LaTeX
$$$\forall x\in E, \|x\| \cdot \|x\| \le \|x x^{\star}\| \Rightarrow E \text{ is a } C^*\text{-ring}$$$
Lean4
theorem of_le_norm_mul_star_self [NonUnitalNormedRing E] [StarRing E] (h : ∀ x : E, ‖x‖ * ‖x‖ ≤ ‖x * x⋆‖) :
CStarRing E :=
have : NormedStarGroup E :=
{
norm_star_le
x := by
obtain (hx | hx) := eq_zero_or_norm_pos x⋆
· simp [hx]
· refine le_of_mul_le_mul_right ?_ hx
simpa [sq, mul_comm ‖x⋆‖] using h x⋆ |>.trans <| norm_mul_le _ _ }
⟨star_involutive.surjective.forall.mpr <| by simpa⟩
