star_isometry
theorem star_isometry :
∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [inst_1 : StarAddMonoid E] [inst_2 : NormedStarGroup E],
Isometry star
The theorem `star_isometry` states that in the context of a normed star group (a group that is both a star add monoid and a seminormed add commutative group), the `star` map, which is a function defined in the star add monoid, is an isometry. In other words, for any two elements in this group, the "distance" (or more accurately, the edistance or extended distance) between their images under the `star` map is the same as the edistance between the elements themselves.
More concisely: In a normed star group, the `star` map is an isometry, meaning the extended distance between any two elements is equal to the extended distance of their images under the `star` map.
|
CstarRing.nnnorm_star_mul_self
theorem CstarRing.nnnorm_star_mul_self :
∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E] [inst_2 : CstarRing E] {x : E},
‖star x * x‖₊ = ‖x‖₊ * ‖x‖₊
This theorem states that for any element `x` of a type `E` that forms a non-unital normed ring, a star ring, and a C* ring, the non-negative norm of the product of the star of `x` and `x` itself is equal to the product of the non-negative norm of `x` with itself. In mathematical notation, this can be expressed as ‖star(x) * x‖₊ = ‖x‖₊ * ‖x‖₊.
More concisely: For any element `x` in a normed ring that is also a star ring and a C* ring, the norm of the product of `x`'s adjoint and `x` equals the square of `x`'s norm.
|