IsSMulRegular.mul_and_mul_iff
theorem IsSMulRegular.mul_and_mul_iff :
∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [inst_2 : IsScalarTower R R M],
IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
In the context of a scalar multiplication `SMul` operation on a type `M` by elements of type `R`, two elements `a` and `b` from `R` are said to be `M`-regular if and only if both the product `a * b` and `b * a` are `M`-regular. Here, an element is `M`-regular if multiplication by this element on the left is an injective (or one-to-one) mapping from `M` to `M`. This is under the assumptions that `R` has a multiplication operation `Mul`, and `R` forms a scalar tower over `M`, which means that scalar multiplication by elements of `R` on `M` is compatible with the multiplication operation in `R`.
More concisely: Two elements of a ring `R` are `M`-regular for scalar multiplication on type `M` if and only if their products in `R` are both `M`-regular and `M` has a one-to-one scalar multiplication by these elements.
|
IsSMulRegular.of_smul_eq_one
theorem IsSMulRegular.of_smul_eq_one :
∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [inst : Monoid S] [inst_1 : SMul R M]
[inst_2 : SMul R S] [inst_3 : MulAction S M] [inst_4 : IsScalarTower R S M], a • s = 1 → IsSMulRegular M s
The theorem `IsSMulRegular.of_smul_eq_one` states that if we have an element `s` from the type `S` such that it admits a left inverse `a` in `R` (i.e., the scalar multiplication of `a` and `s` equals the multiplicative identity `1`), then `s` is a `M`-regular element. Here, an `M`-regular element is defined for any type `R` with a scalar multiplication (`SMul`) operation on `M`. It is an element `c` such that when we multiply any element from `M` on the left by `c`, it results in a unique element in `M`, meaning that the map from `M` to `M` via multiplication by `c` is injective. This theorem is stated under the assumptions that `S` forms a monoid structure (`Monoid S`), the types `R, S, M` have a scalar multiplication operation (`SMul R M` and `SMul R S`), there is an action of `S` on `M` (`MulAction S M`), and `R, S, M` forms a scalar tower (`IsScalarTower R S M`).
More concisely: If an element `s` in a monoid `S` has a left inverse in `R` that scalarly multiplies `s` to `1` in `M`, then `s` is an `M`-regular element in the scalar tower `(R, S, M)`.
|
isSMulRegular_of_group
theorem isSMulRegular_of_group :
∀ {R : Type u_1} {G : Type u_4} [inst : Group G] [inst_1 : MulAction G R] (g : G), IsSMulRegular R g
This theorem states that for any group `G` acting on a type `R`, every element `g` of the group `G` is regular. Here, an element `g` is said to be regular if the left multiplication by `g` is an injective function from `R` to `R`. This property is ensured by the existence of inverses in groups, even though there is no `LeftCancelSMul` typeclass.
More concisely: In any group action on a type, every group element is regular, that is, the left multiplication by the element is an injection.
|
IsSMulRegular.subsingleton
theorem IsSMulRegular.subsingleton :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
IsSMulRegular M 0 → Subsingleton M
The theorem `IsSMulRegular.subsingleton` states that for any types `R` and `M`, given a `MonoidWithZero` structure on `R`, a `Zero` structure on `M`, and a `MulActionWithZero` structure on `R` and `M`, if the element `0` of `R` is `M`-regular (i.e., left multiplication by `0` is an injective function from `M` to `M`), then `M` must be a subsingleton (i.e., `M` has at most one element). In other words, the only way that multiplication by `0` can be injective is if there is at most one element to "hit" in the first place.
More concisely: If a monoid with zero `R` acts regularly on a type `M` with zero via multiplication, and `0` in `R` is left-injective on `M`, then `M` is a subsingleton.
|
isLeftRegular_iff
theorem isLeftRegular_iff : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsLeftRegular a ↔ IsSMulRegular R a
The theorem `isLeftRegular_iff` states that for any type `R` that supports multiplication and any element `a` of `R`, `a` is a left-regular element if and only if `a` is an `R`-regular element. In other words, the property of left-regularity on `R` (which means that multiplication on the left by `a` is injective) is equivalent to the `R`-regularity of `R` itself (which means that scalar multiplication by `a` is an injective map from `R` to `R`).
More concisely: A left-regular element in a ring is equivalent to an `R`-regular element.
|
IsSMulRegular.pow_iff
theorem IsSMulRegular.pow_iff :
∀ {R : Type u_1} {M : Type u_3} {a : R} [inst : Monoid R] [inst_1 : MulAction R M] {n : ℕ},
0 < n → (IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a)
The theorem `IsSMulRegular.pow_iff` states that for any given types `R` and `M`, any element `a` of type `R`, having an instance of `Monoid` for `R` and an instance of `MulAction` for `R` and `M`, and any natural number `n` greater than zero, an element `a` is `M`-regular if and only if a positive power of `a` is `M`-regular. This means that the property of `M`-regularity for an element `a` is preserved under taking positive powers of `a`. In mathematical terms, if `c` is an `M`-regular element, it means that the function defined by left multiplication by `c` on `M` is injective. The theorem thus establishes the equivalence of `M`-regularity of `a` and its positive powers.
More concisely: For any Monoid R, MulAction M over R, and natural number n > 0, an element a of R is M-regular if and only if the n-th power of a is M-regular.
|
IsSMulRegular.mul_iff
theorem IsSMulRegular.mul_iff :
∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : CommSemigroup R] [inst_1 : SMul R M]
[inst_2 : IsScalarTower R R M], IsSMulRegular M (a * b) ↔ IsSMulRegular M a ∧ IsSMulRegular M b
The theorem `IsSMulRegular.mul_iff` states that for any types `R` and `M`, and for any elements `a` and `b` in `R`, under the conditions that `R` is a commutative semigroup, `M` is a scalar multiplication space over `R`, and `R` acts on `M` through scalar multiplication, an element formed by the product of `a` and `b` (`a * b`) is `M`-regular if and only if both `a` and `b` are `M`-regular themselves. Here, an `M`-regular element is defined as an element such that multiplication on the left by it results in an injective map from `M` to `M`.
More concisely: For any commutative semigroup R, scalar multiplication space M, and elements a and b in R, the product a * b is M-regular if and only if both a and b are M-regular.
|
IsSMulRegular.of_mul
theorem IsSMulRegular.of_mul :
∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : SMul R M] [inst_1 : Mul R] [inst_2 : IsScalarTower R R M],
IsSMulRegular M (a * b) → IsSMulRegular M b
The theorem `IsSMulRegular.of_mul` states that for any types `R` and `M`, given any elements `a` and `b` of type `R`, and assuming that the type `R` has an operation of scalar multiplication on `M`, an operation of multiplication, and that `R` is a scalar tower over `M`. If the product `a * b` is an `M`-regular element (an element `c` such that multiplication on the left by `c` is an injective map `M → M`), then `b` is also an `M`-regular element.
More concisely: If `a * b` is an `M`-regular element in a commutative ring `R` with scalar multiplication on `M`, then `b` is also an `M`-regular element.
|
IsSMulRegular.one
theorem IsSMulRegular.one :
∀ {R : Type u_1} (M : Type u_3) [inst : Monoid R] [inst_1 : MulAction R M], IsSMulRegular M 1
The theorem `IsSMulRegular.one` states that for any types `R` and `M`, and with the assumption that `R` is a monoid and there is a multiplication action from `R` to `M`, the number 1 is always `M`-regular. In terms of mathematics, an element is `M`-regular if multiplying by that element on the left is an injective (one-to-one) function from `M` to `M`. Therefore, this theorem is saying that multiplying by 1 on the left is always a one-to-one function.
More concisely: For any monoid `R` acting on a type `M` via multiplication, the multiplicative identity 1 is a left-inverse for the multiplication operation, hence is `M`-regular.
|
IsSMulRegular.of_mul_eq_one
theorem IsSMulRegular.of_mul_eq_one :
∀ {R : Type u_1} {M : Type u_3} {a b : R} [inst : Monoid R] [inst_1 : MulAction R M],
a * b = 1 → IsSMulRegular M b
This theorem states that for any types `R` and `M`, and any elements `a` and `b` of `R`, given that `R` forms a monoid and `M` is a `R`-mul_action, if `a` and `b` multiply to give the identity of `R`, then `b` is an `M`-regular element. In other words, if there exists a left inverse `a` for an element `b` in a monoid `R`, then multiplication by `b` on the left is an injective function from `M` to `M` under the `R`-mul_action context.
More concisely: If `R` is a monoid and `M` is an `R`-module, and there exists an element `a` in `R` such that `a * b = id_R` (identity of `R`), then `b` is an `M`-regular element.
|
IsSMulRegular.zero
theorem IsSMulRegular.zero :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M]
[sM : Subsingleton M], IsSMulRegular M 0
The theorem `IsSMulRegular.zero` asserts that the zero element (`0`) is `M`-regular when `M` is trivial. Here `M`-regular means that multiplication by an element on the left results in an injective (or one-to-one) function from `M` to `M`. Specifically, for any type `R` that has a structure of `MonoidWithZero` (a monoid with an additional zero element that is an absorbing element for the multiplication), and any type `M` that has a zero element and a multiplication action by `R` that respects zero, if `M` is a subsingleton (i.e., `M` has at most one element), then the zero element of `R` is `M`-regular.
More concisely: If `M` is a subsingleton type with a zero element and `R` is a monoid with zero, then the zero element of `R` is injective when acting as multiplication on `M`.
|
IsUnit.isSMulRegular
theorem IsUnit.isSMulRegular :
∀ {R : Type u_1} (M : Type u_3) {a : R} [inst : Monoid R] [inst_1 : MulAction R M], IsUnit a → IsSMulRegular M a
The theorem `IsUnit.isSMulRegular` states that for any type `R` equipped with a monoid structure and any type `M` equipped with a multiplication action by `R`, if an element `a` of `R` is a unit (meaning it has a two-sided inverse), then `a` is `M`-regular. In other words, multiplication on the left by `a` is an injective function from `M` to `M`. This means that multiplying different elements of `M` by the unit `a` will give distinct results, hence preserving the uniqueness of elements under this operation.
More concisely: If `a` is a unit in the monoid `R` and `M` is an `R`-module, then `a`'s multiplication action on `M` is left-injective.
|
IsSMulRegular.of_smul
theorem IsSMulRegular.of_smul :
∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {s : S} [inst : SMul R M] [inst_1 : SMul R S] [inst_2 : SMul S M]
[inst : IsScalarTower R S M] (a : R), IsSMulRegular M (a • s) → IsSMulRegular M s
The theorem states that for any types `R`, `S`, and `M`, and for any given element `s` of type `S`, if `s` becomes `M`-regular when it is left-multiplied with an `M`-regular element `a` of type `R`, then `s` itself is `M`-regular. Here, `M`-regularity of an element means that left-multiplication with that element induces an injective (or one-to-one) function from `M` to `M`. The theorem assumes scalar multiplication structures on `R` and `S` with `M` respectively, and it also assumes that `R`, `S` and `M` form a scalar tower, which means that multiplication of scalars is associative across the types `R`, `S`, and `M`.
More concisely: If `s` in `S` becomes `M`-regular when left-multiplied with an `M`-regular element `a` in `R`, then `s` is `M`-regular, given scalar multiplication structures and `M` being a common submodule of `R` and `S` forming a scalar tower.
|
IsSMulRegular.zero_iff_subsingleton
theorem IsSMulRegular.zero_iff_subsingleton :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
IsSMulRegular M 0 ↔ Subsingleton M
The theorem `IsSMulRegular.zero_iff_subsingleton` states that for any given types `R` and `M`, with `R` being a monoid with zero, and `M` having a zero and supporting a multiplication action by elements of `R` that respects zero, the zero element in `R` is `M`-regular if and only if `M` is a subsingleton. In other words, the zero element of `R` is `M`-regular; that is, multiplication on the left by zero is an injective function from `M` to `M`, if and only if `M` is a subsingleton type; that is, a type with at most one element.
More concisely: For a monoid `R` with zero and a type `M` with zero and left multiplication action by `R`, the zero element of `R` is injective on `M` if and only if `M` is a singleton.
|
IsSMulRegular.smul
theorem IsSMulRegular.smul :
∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} {s : S} [inst : SMul R M] [inst_1 : SMul R S]
[inst_2 : SMul S M] [inst_3 : IsScalarTower R S M],
IsSMulRegular M a → IsSMulRegular M s → IsSMulRegular M (a • s)
This theorem states that the product of `M`-regular elements is `M`-regular. In other words, for any types `R`, `S`, `M`, and any elements `a` of `R` and `s` of `S`, given the scalar multiplication operations from `R` to `M`, `R` to `S`, and `S` to `M` and the scalar tower property for these types, if `a` and `s` are `M`-regular (meaning that left multiplication by either `a` or `s` is an injective function from `M` to `M`), then the product `a • s` is also `M`-regular.
More concisely: If `a` and `s` are `M`-regular elements in types `R` and `S`, respectively, then their product `a • s` is also an `M`-regular element.
|
IsSMulRegular.pow
theorem IsSMulRegular.pow :
∀ {R : Type u_1} {M : Type u_3} {a : R} [inst : Monoid R] [inst_1 : MulAction R M] (n : ℕ),
IsSMulRegular M a → IsSMulRegular M (a ^ n)
This theorem states that for any types `R` and `M`, and any natural number `n`, if `a` is an `M`-regular element of `R` (meaning that left-multiplication by `a` is an injective map from `M` to `M`), then `a` to the power of `n` is also an `M`-regular element of `R`. This holds under the conditions that `R` is a monoid and that there is a multiplication action of `R` on `M`. Put more simply, any power of an `M`-regular element is also `M`-regular.
More concisely: If `a` is an `M`-regular element of monoid `R` with multiplication action on `M`, then `a^n` is also an `M`-regular element of `R` for any natural number `n`.
|
isRightRegular_iff
theorem isRightRegular_iff :
∀ {R : Type u_1} [inst : Mul R] {a : R}, IsRightRegular a ↔ IsSMulRegular R (MulOpposite.op a)
The theorem `isRightRegular_iff` states that for any type `R` with a multiplication operation, and any element `a` of `R`, the element `a` is right-regular (meaning that multiplication by `a` on the right is an injective function) if and only if `a` is regular with respect to the scalar multiplication operation of `R` in the opposite multiplication order, i.e., `Rᵐᵒᵖ`. In other words, it establishes an equivalence between right-regular multiplication on `R` and `Rᵐᵒᵖ`-regularity of `R` itself.
More concisely: For any type `R` with multiplication and an element `a` in `R`, `a` is right-regular if and only if `R` is `Rᵐᵒᵖ`-regular with respect to `a`.
|
IsSMulRegular.not_zero_iff
theorem IsSMulRegular.not_zero_iff :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
¬IsSMulRegular M 0 ↔ Nontrivial M
The theorem `IsSMulRegular.not_zero_iff` states that for any monoid with zero `R` and any type `M` equipped with a zero and an action of `R` that is compatible with zero, the `0` element of `R` is not `M`-regular iff `M` is non-trivial. Here, an element `c` of `R` being `M`-regular means that multiplication by `c` on the left is an injective (one-to-one) function from `M` to `M`. Moreover, a module `M` is said to be non-trivial if it has at least two distinct elements.
More concisely: For a monoid with zero R and an R-module M with at least two elements, the zero element of R is not left multiplication regular on M if and only if M is non-trivial.
|
Units.isSMulRegular
theorem Units.isSMulRegular :
∀ {R : Type u_1} (M : Type u_3) [inst : Monoid R] [inst_1 : MulAction R M] (a : Rˣ), IsSMulRegular M ↑a
This theorem states that for any monoid `R` and any type `M` which is a `MulAction` of `R`, any unit `a` in `R` is `M`-regular. In other words, for any such `a`, multiplication on the left by `a` is an injective function from `M` to `M`. This means that for any two elements `x` and `y` in `M`, if `a * x = a * y` then `x = y`. Where `Rˣ` is the group of units (invertible elements) in `R` and an `M`-regular element is defined as an element `c` such that multiplication on the left by `c` is an injective map `M → M`.
More concisely: For any monoid `R` and `M` being an `MulAction` of `R`, any unit `a` in `R` makes left multiplication by `a` an injective function on `M`.
|
IsSMulRegular.not_zero
theorem IsSMulRegular.not_zero :
∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M]
[nM : Nontrivial M], ¬IsSMulRegular M 0
The theorem `IsSMulRegular.not_zero` states that the zero element is not `M`-regular for a non-trivial module `M`. In the context of a module `M` over a monoid with zero `R`, an `M`-regular element is one for which multiplication on the left is an injective function from `M` to `M`. Thus, this theorem asserts that zero does not have this property; that is, there exists at least one pair of distinct elements of `M` which both become zero when multiplied by zero, violating the injectivity condition.
More concisely: The theorem `IsSMulRegular.not_zero` asserts that the zero element is not injective under left multiplication in a non-trivial module over a monoid with zero.
|
IsSMulRegular.smul_iff
theorem IsSMulRegular.smul_iff :
∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {a : R} [inst : SMul R M] [inst_1 : SMul R S] [inst_2 : SMul S M]
[inst_3 : IsScalarTower R S M] (b : S), IsSMulRegular M a → (IsSMulRegular M (a • b) ↔ IsSMulRegular M b)
The theorem `IsSMulRegular.smul_iff` states the following: For any types `R`, `S`, and `M`, and for any elements `a` of type `R` and `b` of type `S`, given certain scalar multiplication structures on `R`, `S`, and `M`, as well as a scalar tower structure on `R`, `S`, and `M`, if `a` is an `M`-regular element, then `a` scalarmultiplied by `b` is `M`-regular if and only if `b` is `M`-regular. Here, an `M`-regular element is defined as an element `c` for which multiplication on the left by `c` is an injective map from `M` to `M`.
More concisely: For elements `a` in `R` and `b` in `S` with `M`-regular scalars, `a` is `M`-regular implies `a * b` is `M`-regular if and only if `b` is `M`-regular.
|