MonoidWithZeroHom.congr_arg
theorem MonoidWithZeroHom.congr_arg :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β) {x y : α},
x = y → f x = f y
This theorem states that for any two types `α` and `β` that belong to the `MulZeroOneClass` (a class of elements with multiplication, zero and one), given a monoid homomorphism (i.e., a structure-preserving map) `f` from `α` to `β`, and any two elements `x` and `y` of `α`, if `x` equals `y`, then `f(x)` equals `f(y)`. In other words, this theorem is about the property of a monoid homomorphism preserving equality: equal arguments yield equal results.
More concisely: Given monoid homomorphisms between types `α` and `β` in the `MulZeroOneClass`, if `α` elements `x` and `y` are equal, then `f(x) = f(y)` for all such homomorphisms `f`.
|
MonoidWithZeroHom.congr_fun
theorem MonoidWithZeroHom.congr_fun :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {f g : α →*₀ β},
f = g → ∀ (x : α), f x = g x
The `MonoidWithZeroHom.congr_fun` theorem states that for any two monoid-with-zero homomorphisms `f` and `g` from a type `α` to a type `β`, where `α` and `β` are both `MulZeroOneClass` types, if `f` equals `g`, then for every element `x` of type `α`, `f(x)` must equal `g(x)`. In other words, it asserts the principle of function extensionality for monoid-with-zero homomorphisms: two such functions are equal if and only if they agree on all inputs.
More concisely: If `f` and `g` are equal monoid-with-zero homomorphisms from a `MulZeroOneClass` type `α` to another `MulZeroOneClass` type `β`, then `f(x) = g(x)` for all `x` in `α`.
|
MonoidWithZeroHom.ext_iff
theorem MonoidWithZeroHom.ext_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] {f g : α →*₀ β},
f = g ↔ ∀ (x : α), f x = g x
This theorem states that for any two functions `f` and `g` of type `α →*₀ β` (where `α` and `β` are instances of the MulZeroOneClass, meaning they have multiplication, one, and zero operations), `f` and `g` are equal if and only if for every element `x` of type `α`, `f(x)` is equal to `g(x)`. In other words, if two homomorphisms from a multiplicative monoid with zero map every element to the same other element in another such monoid, they are indeed the same function.
More concisely: Two functions `f` and `g` of type `α →*₀ β` are equal if and only if for all `x` in `α`, `f(x) = g(x)`.
|
MonoidWithZeroHom.map_one
theorem MonoidWithZeroHom.map_one :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), f 1 = 1 := by
sorry
This theorem states that for any given `MonoidWithZeroHom` (a homomorphism of monoids with zero), the image under this homomorphism of the unity (or identity) element of the source monoid is equal to the unity element of the target monoid. In simpler terms, this theorem says that if `f` is a function mapping one multiplicative monoid with a zero element to another, then applying `f` to the number one in the first monoid will give you the number one in the second monoid. This is a generalization of the property that the identity element is preserved under a group homomorphism.
More concisely: For any `MonoidWithZeroHom` homomorphism `f` between monoids with zero, `f (1) = 1`, where `1` represents the identity elements of the respective monoids.
|
MonoidWithZeroHom.map_one'
theorem MonoidWithZeroHom.map_one' :
∀ {α : Type u_6} {β : Type u_7} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (self : α →*₀ β),
self.toFun 1 = 1
This theorem states that for any two types `α` and `β` that both have a multiplication, zero, and one structure (denoted as `MulZeroOneClass`), any function (`self`) that is a monoid homomorphism from `α` to `β` that also preserves zero (denoted as `α →*₀ β`), will map the element `1` from `α` to the element `1` in `β`. In simpler terms, this theorem guarantees that a monoid homomorphism between two multiplicative structures with zero and one will always preserve the identity element, `1`.
More concisely: Given types `α` and `β` with Multiplicative Monoid, Zero, and One structures, and a monoid homomorphism `self : α →*₀ β`, then `self 1 = 1`.
|
MonoidWithZeroHom.map_mul'
theorem MonoidWithZeroHom.map_mul' :
∀ {α : Type u_6} {β : Type u_7} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (self : α →*₀ β) (x y : α),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that a given function, which maps elements from one multiplication-zero-one class to another, preserves the multiplication operation. In other words, for any elements `x` and `y` of type `α`, the result of applying the function to the product of `x` and `y` (`x * y`) is the same as the product of the results of applying the function to `x` and `y` separately (`self.toFun x * self.toFun y`). This applies to any types `α` and `β` that have a multiplication operation, a zero element, and a one element (i.e., they are instances of the `MulZeroOneClass`).
More concisely: For any functions `self : α → β` between multiplicative zero-one classes `α` and `β`, `self (x * y) = self x * self y` for all `x, y` in `α`.
|
MonoidWithZeroHom.ext
theorem MonoidWithZeroHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] ⦃f g : α →*₀ β⦄,
(∀ (x : α), f x = g x) → f = g
This theorem, `MonoidWithZeroHom.ext`, states that for any two types `α` and `β`, where both types have a multiplication, zero, and one operation (i.e., they are instances of the `MulZeroOneClass`), if you have two monoid homomorphisms (`f` and `g`) from `α` to `β` such that for every element `x` in `α`, `f(x)` equals `g(x)`, then `f` and `g` must be the same monoid homomorphism. In other words, two monoid homomorphisms between two `MulZeroOneClass` types are equal if they map every element to the same value.
More concisely: If `f` and `g` are monoid homomorphisms from a `MulZeroOneClass` type `α` to another `MulZeroOneClass` type `β` such that `f(x) = g(x)` for all `x` in `α`, then `f` and `g` are equal.
|
MonoidWithZeroHom.coe_inj
theorem MonoidWithZeroHom.coe_inj :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] ⦃f g : α →*₀ β⦄,
⇑f = ⇑g → f = g
This theorem states that for any two types `α` and `β`, both of which are instances of the `MulZeroOneClass` (meaning that they support multiplication, have a zero, and have a one), any pair of monoid-with-zero homomorphisms `f` and `g` from `α` to `β` are equal if and only if their corresponding function applications (denoted by `⇑f` and `⇑g`) are equal. "Monoid-with-zero" homomorphism refers to a structure-preserving function between two algebraic structures (monoids-with-zero in this case) that respects the operations of the structures (here, multiplication, zero, and one).
More concisely: For any types `α` and `β` instances of `MulZeroOneClass`, and any two monoid-with-zero homomorphisms `f` and `g` from `α` to `β`, `f = g` if and only if `⇑f = ⇑g`.
|
MonoidWithZeroHom.map_mul
theorem MonoidWithZeroHom.map_mul :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β) (a b : α),
f (a * b) = f a * f b
This theorem states that for any two types `α` and `β` that are instances of the `MulZeroOneClass` (which means they support multiplication, have a zero element, and have a one element), any monoid homomorphism with zero `f` from `α` to `β` preserves multiplication. In other words, if `a` and `b` are elements of `α`, then the image of the product `a * b` under `f` is the product of the images of `a` and `b` under `f`. This is a property that characterizes monoid homomorphisms in mathematics, specifically those that also map the zero of the source structure to the zero of the target structure.
More concisely: For any monoid homomorphisms f between MulZeroOneClasses α and β, a * b maps to f a * f b, where a, b are elements of α and * denotes multiplication.
|
MonoidWithZeroHom.map_zero
theorem MonoidWithZeroHom.map_zero :
∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β), f 0 = 0 := by
sorry
This theorem states that for any monoid homomorphism `f` from a type `α` to a type `β`, where both `α` and `β` have structures of `MulZeroOneClass` (meaning they have multiplication operation, and elements zero and one with certain properties), the image of `0` under `f` is `0`. In other words, this homomorphism preserves the zero element while mapping from `α` to `β`.
More concisely: For any monoid homomorphism `f` from a `MulZeroOneClass` type `α` to a `MulZeroOneClass` type `β`, `f 0 = 0`.
|