MulSemiringAction.smul_one
theorem MulSemiringAction.smul_one :
∀ {M : Type u} {R : Type v} [inst : Monoid M] [inst_1 : Semiring R] [self : MulSemiringAction M R] (g : M),
g • 1 = 1
This theorem states that for any monoid `M` and any semiring `R`, if `R` is a semiring over `M` (meaning `M` and `R` form a MulSemiringAction), then multiplying `1` from `R` by any element `g` from `M` (denoted as `g • 1`) will always result in `1`. This holds for all elements `g` in `M`. In other words, a scalar multiplication of `1` by any element in the monoid leaves `1` unchanged.
More concisely: For any monoid `M` and semiring `R` over `M`, the scalar multiplication of `1` from `R` by any element `g` in `M` results in `1`.
|
smul_inv''
theorem smul_inv'' :
∀ {M : Type u_1} [inst : Monoid M] {F : Type v} [inst_1 : DivisionRing F] [inst_2 : MulSemiringAction M F] (x : M)
(m : F), x • m⁻¹ = (x • m)⁻¹
The theorem `smul_inv''` states that for any given type `M` that forms a Monoid, a type `F` that forms a Division Ring, and an action of `M` on `F` that forms a Multiplicative Semiring Action, for every element `x` of `M` and every element `m` of `F`, the scalar multiplication of `x` and the multiplicative inverse of `m` is equal to the multiplicative inverse of the scalar multiplication of `x` and `m`. In mathematical terms, it says that `x` multiplied by the inverse of `m` is the same as the inverse of `x` multiplied by `m`. This is a property related to the distributive law in the context of division rings and monoids, with a specific focus on scalar multiplication.
More concisely: For any monoid `M`, division ring `F`, and multiplicative semiring action of `M` on `F`, for all `x in M` and `m in F`, `x * m^(-1) = m^(-1) * x`.
|
MulSemiringAction.smul_mul
theorem MulSemiringAction.smul_mul :
∀ {M : Type u} {R : Type v} [inst : Monoid M] [inst_1 : Semiring R] [self : MulSemiringAction M R] (g : M)
(x y : R), g • (x * y) = g • x * g • y
This theorem, `MulSemiringAction.smul_mul`, states that for any types `M` and `R`, where `M` is a Monoid and `R` is a Semiring, and where `M` acts on `R` through scalar multiplication (a `MulSemiringAction`), scalar multiplication distributes over the multiplication from `R`. Specifically, for any elements `g` of `M` and `x`, `y` of `R`, multiplying `g` with the product of `x` and `y` (`g • (x * y)`) is equal to the product of `g` multiplied with `x` and `g` multiplied with `y` (`g • x * g • y`). This is a fundamental property in abstract algebra that ensures the consistency of scalar multiplication and multiplication in the context of a semiring action.
More concisely: For any Monoid `M` acting on a Semiring `R` through scalar multiplication (MulSemiringAction), the scalar multiplication distributes over the multiplication of `R`, i.e., `g • (x * y) = g • x * g • y` for all `g` in `M` and `x`, `y` in `R`.
|