CentroidHom.ext
theorem CentroidHom.ext :
∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] {f g : CentroidHom α}, (∀ (a : α), f a = g a) → f = g := by
sorry
This theorem, `CentroidHom.ext`, states that for all types `α` in a non-unital non-associative semiring, if two centroid homomorphisms `f` and `g` from `α` are such that they produce the same output for every element of `α`, then `f` and `g` are the same function. In other words, two centroid homomorphisms are equal if they have the same effect on all elements of their domain.
More concisely: If `α` is a non-unital non-associative semiring and centroid homomorphisms `f` and `g` from `α` agree on all elements, then `f` equals `g`.
|
CentroidHomClass.map_mul_left
theorem CentroidHomClass.map_mul_left :
∀ {F : Type u_6} {α : Type u_7} [inst : NonUnitalNonAssocSemiring α] [inst_1 : FunLike F α α]
[self : CentroidHomClass F α] (f : F) (a b : α), f (a * b) = a * f b
The theorem `CentroidHomClass.map_mul_left` states that for any types `F` and `α`, where `α` forms a non-unital, non-associative semiring and `F` is a function-like type from `α` to `α`, and for any instance of `CentroidHomClass` for `F` and `α`, the action of any function `f : F` on the product of two elements `a` and `b` of `α` (`f (a * b)`) is the same as the product of `a` and the action of `f` on `b` (`a * f b`). In other words, the centroid homomorphism `f` commutes with left multiplication in this non-unital non-associative semiring.
More concisely: For any non-unital, non-associative semiring `α` and function-like type `F` over `α`, the centroid homomorphism `f : F` satisfies `f (a * b) = a * f b`.
|
CentroidHom.map_mul_right'
theorem CentroidHom.map_mul_right' :
∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a b : α),
self.toFun (a * b) = self.toFun a * b
This theorem states the commutativity of centroid homomorphisms with right multiplication in a non-unital, non-associative semiring. Specifically, for any type `α` with a `NonUnitalNonAssocSemiring` structure, any centroid homomorphism (`self`), and any two elements `a` and `b` of `α`, applying the centroid homomorphism to the product of `a` and `b` (`a * b`) is equal to applying the centroid homomorphism to `a` and then multiplying by `b` (i.e., `self.toFun a * b`).
More concisely: For any non-unital, non-associative semiring `α` and its centroid homomorphism `self`, the centroid homomorphism commutes with right multiplication, i.e., `self (a * b) = self a * b` for all `a, b` in `α`.
|
CentroidHomClass.map_mul_right
theorem CentroidHomClass.map_mul_right :
∀ {F : Type u_6} {α : Type u_7} [inst : NonUnitalNonAssocSemiring α] [inst_1 : FunLike F α α]
[self : CentroidHomClass F α] (f : F) (a b : α), f (a * b) = f a * b
The theorem `CentroidHomClass.map_mul_right` states that for every type `F` and `α`, given that `α` is a non-unital non-associative semiring and `F` is a type that behaves like a function from `α` to `α`, and that `F` forms a centroid homomorphism on `α`, then for every function `f` of type `F` and every elements `a` and `b` of `α`, the result of applying `f` to the product of `a` and `b` is equal to the product of the result of applying `f` to `a` and `b`. In other words, the centroid homomorphism commutes with right multiplication.
More concisely: For any non-unital non-associative semiring `α` and centroid homomorphism `F` from `α` to `α`, the application of `F` on the product of two elements `a` and `b` is equal to the product of the applications of `F` on `a` and `b`.
|
CentroidHom.toEnd_smul
theorem CentroidHom.toEnd_smul :
∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M]
[inst_2 : DistribMulAction M α] [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α] (m : M)
(x : CentroidHom α), (m • x).toEnd = m • x.toEnd
The theorem `CentroidHom.toEnd_smul` states that for any type `M` which is a monoid, any type `α` which is a non-unital non-associative semiring, and with `α` having a distributive multiplication action by `M` and scalar multiplication on `α` commuting with the multiplication in `α` (i.e., `M`, `α` and `α` form a scalar multiplication commutative class) and `M` being a scalar tower over `α`, for any element `m` in `M` and any centroid homomorphism `x` on `α`, the endomorphism obtained by applying the scalar `m` to `x` and then converting to an endomorphism is the same as first converting `x` to an endomorphism and then applying the scalar `m`. In terms of formulas, the theorem says that for all `m` in `M` and all `x` in `CentroidHom α`, we have `CentroidHom.toEnd (m • x) = m • CentroidHom.toEnd x`.
More concisely: For any monoid `M`, non-unital non-associative semiring `α` with distributive `M`-action and commuting scalar multiplication, and scalar tower `M` over `α`, the endomorphism obtained by applying a scalar `m` in `M` to a centroid homomorphism `x` and then converting to an endomorphism is equal to first converting `x` to an endomorphism and then applying `m`.
|
CentroidHom.map_mul_left'
theorem CentroidHom.map_mul_left' :
∀ {α : Type u_6} [inst : NonUnitalNonAssocSemiring α] (self : CentroidHom α) (a b : α),
self.toFun (a * b) = a * self.toFun b
This theorem is about the commutativity of centroid homomorphisms with left multiplication in a non-unital, non-associative semiring. Specifically, for any type `α` that forms a non-unital, non-associative semiring, any centroid homomorphism `self` on `α`, and any two elements `a` and `b` of `α`, the value of `self` applied to the product of `a` and `b` (`a * b`) is equal to the product of `a` and the value of `self` applied to `b`.
More concisely: For any non-unital, non-associative semiring `α`, any centroid homomorphism `self` over `α`, and all elements `a, b` in `α`, `self (a * b) = a * self b`.
|