IsRegular.pow_iff
theorem IsRegular.pow_iff :
∀ {R : Type u_1} {a : R} [inst : Monoid R] {n : ℕ}, 0 < n → (IsRegular (a ^ n) ↔ IsRegular a)
This theorem states that for any element `a` of a Monoid `R` and a positive integer `n`, `a` is a regular element if and only if some positive power of `a` is regular. In terms of abstract algebra, this means that an element in a mathematical structure (Monoid) is regular if it satisfies certain properties, and these properties remain valid even when the element is raised to a positive power.
More concisely: For any monoid element `a` and positive integer `n`, `a` is regular if and only if some power `a^k` is regular.
|
IsRightRegular.pow_iff
theorem IsRightRegular.pow_iff :
∀ {R : Type u_1} {a : R} [inst : Monoid R] {n : ℕ}, 0 < n → (IsRightRegular (a ^ n) ↔ IsRightRegular a)
The theorem states that for any type `R` that forms a monoid, an element `a` from `R` is right-regular if and only if a positive power of `a` is right-regular. In other words, in a monoid, if multiplying any element by `a` to the power of a positive natural number `n` on the right maintains the distinctiveness of the elements (i.e., it is injective), then the same property holds true when multiplying by `a` itself, and vice versa.
More concisely: For any monoid `R` and element `a` in `R`, `a` is right-regular if and only if for some natural number `n`, the `n`th power of `a` is right-regular in `R`.
|
IsLeftRegular.pow
theorem IsLeftRegular.pow :
∀ {R : Type u_1} {a : R} [inst : Monoid R] (n : ℕ), IsLeftRegular a → IsLeftRegular (a ^ n)
This theorem states that any power of a left-regular element remains left-regular. In more detail, let `R` be a type with a multiplication operation forming a monoid. If `a` is an element of `R` that is left-regular (i.e., multiplication on the left by `a` is injective), then for any natural number `n`, `a` raised to the power `n` is also left-regular.
More concisely: If `a` is a left-regular element in a monoid `R`, then for all natural numbers `n`, `a^n` is also left-regular.
|
IsRegular.pow
theorem IsRegular.pow : ∀ {R : Type u_1} {a : R} [inst : Monoid R] (n : ℕ), IsRegular a → IsRegular (a ^ n)
This theorem states that for any type `R` that forms a monoid and any element `a` of `R`, if `a` is a regular element, then any power of `a`, denoted as `a^n` for any non-negative integer `n`, is also a regular element. Here, a regular element in a monoid is one that satisfies certain algebraic properties, providing a useful structural insight into the monoid.
More concisely: In a monoid, if `a` is a regular element, then for every non-negative integer `n`, `a^n` is also a regular element.
|
IsRightRegular.pow
theorem IsRightRegular.pow :
∀ {R : Type u_1} {a : R} [inst : Monoid R] (n : ℕ), IsRightRegular a → IsRightRegular (a ^ n)
This theorem states that for any type `R` that forms a monoid under multiplication, if an element `a` of `R` is right-regular, then any power of `a` is also right-regular. In other words, if multiplication on the right by `a` is injective (it maps distinct inputs to distinct outputs), then multiplication on the right by `a` raised to any natural number power is also injective.
More concisely: If `R` is a monoid and `a` in `R` is right-regular, then for all natural numbers `n`, `a` right-multiplied by `a` `n` times is injective.
|
IsLeftRegular.pow_iff
theorem IsLeftRegular.pow_iff :
∀ {R : Type u_1} {a : R} [inst : Monoid R] {n : ℕ}, 0 < n → (IsLeftRegular (a ^ n) ↔ IsLeftRegular a)
The theorem states that an element `a` in a monoid `R` is left-regular if and only if a positive power of `a` is also left-regular. Here, 'left-regular' refers to elements where multiplication on the left by the element is an injective function. The natural number `n` represents the exponent to which `a` is raised, and it is required to be greater than zero. This means that the property of left-regularity is preserved under positive exponentiation in a monoid.
More concisely: If `a` is left-regular in a monoid `R`, then for any positive integer `n`, `a^n` is also left-regular in `R`.
|