RingNorm.eq_zero_of_map_eq_zero'
theorem RingNorm.eq_zero_of_map_eq_zero' :
∀ {R : Type u_4} [inst : NonUnitalNonAssocRing R] (self : RingNorm R) (x : R), self.toFun x = 0 → x = 0
The theorem `RingNorm.eq_zero_of_map_eq_zero'` states that for any non-unital, non-associative ring `R` and any `RingNorm` on `R`, if the image of an element `x` from `R` under the `RingNorm` is zero, then the element `x` itself must be zero. In other words, no non-zero element of `R` can map to zero under the given `RingNorm`.
More concisely: If `R` is a non-unital, non-associative ring and `RingNorm` is a norm on `R`, then for all `x` in `R`, `RingNorm x = 0` implies `x = 0`.
|
MulRingSeminorm.map_mul'
theorem MulRingSeminorm.map_mul' :
∀ {R : Type u_4} [inst : NonAssocRing R] (self : MulRingSeminorm R) (x y : R),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem asserts that a given multiplicative ring seminorm, denoted as `self`, maintains the structure of multiplication in the ring `R`. Specifically, for any elements `x` and `y` in the ring `R`, applying the function `self.toFun` on the product of `x` and `y` is equivalent to first applying `self.toFun` individually on `x` and `y` and then taking the product of the results. In mathematical notation, this property can be written as `self.toFun (x * y) = self.toFun x * self.toFun y`. The ring `R` is assumed to be a non-associative ring in this context.
More concisely: For a multiplicative ring seminorm `self` on a non-associative ring `R`, `self.toFun (x * y) = self.toFun x * self.toFun y` for all `x, y ∈ R`.
|
RingSeminorm.mul_le'
theorem RingSeminorm.mul_le' :
∀ {R : Type u_4} [inst : NonUnitalNonAssocRing R] (self : RingSeminorm R) (x y : R),
self.toFun (x * y) ≤ self.toFun x * self.toFun y
This theorem states that for any arbitrary ring `R` (which is a non-unital, non-associative ring) and any `RingSeminorm` on `R`, the norm of the product of any two elements `x` and `y` from the ring is always less than or equal to the product of the norms of `x` and `y`. This property is known as sub-multiplicativity.
More concisely: For any non-unital ring R and RingSeminorm norm on R, norm(x * y) ≤ norm(x) * norm(y) for all x, y ∈ R.
|
MulRingSeminorm.map_one'
theorem MulRingSeminorm.map_one' :
∀ {R : Type u_4} [inst : NonAssocRing R] (self : MulRingSeminorm R), self.toFun 1 = 1
This theorem states that for any type `R` that forms a non-associative ring, any multiplicative ring seminorm `self` applied to the multiplicative identity (1) will yield the multiplicative identity itself (1). In other words, the seminorm function preserves the multiplicative identity in the ring.
More concisely: For any non-associative ring type `R` and multiplicative ring seminorm `self`, `self 1 = 1`.
|
MulRingNorm.eq_zero_of_map_eq_zero'
theorem MulRingNorm.eq_zero_of_map_eq_zero' :
∀ {R : Type u_4} [inst : NonAssocRing R] (self : MulRingNorm R) (x : R), self.toFun x = 0 → x = 0
This theorem states that for any non-associative ring `R` and an element `x` of `R`, if the image of `x` under a given seminorm is zero, then `x` itself must be zero. In other words, it asserts that a seminorm in a non-associative ring maps only the zero element to zero, providing a specific property of seminorms in the context of non-associative rings.
More concisely: In a non-associative ring, if a seminorm maps an element to zero, then that element is the additive identity (zero).
|