AddSubmonoid.gc_map_comap
theorem AddSubmonoid.gc_map_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F),
GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)
The theorem `AddSubmonoid.gc_map_comap` states that for any types `M` and `N` that are additive monoids (i.e., they have a zero and an addition operation), and any function-like `f` that is an additive monoid homomorphism from `M` to `N`, there is a Galois connection between the map of an additive submonoid along `f` and the preimage of an additive submonoid along `f`. In other words, for an additive submonoid `S` of `M` and `T` of `N`, the image of `S` under `f` is a submonoid of `T` if and only if `S` is a submonoid of the preimage of `T` under `f`. A Galois connection is a relationship between two order-preserving functions that captures the idea of an adjoint functor in category theory.
More concisely: For additive monoids M and N, and additive monoid homomorphism f from M to N, there is a Galois connection between the image of additive submonoids of M under f and the preimage of additive submonoids of N under f.
|
MonoidHom.map_mclosure
theorem MonoidHom.map_mclosure :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F) (s : Set M),
Submonoid.map f (Submonoid.closure s) = Submonoid.closure (⇑f '' s)
The theorem `MonoidHom.map_mclosure` states that for any two types `M` and `N` that are instances of the `MulOneClass` (which means they are monoids), any instance `F` that is a function-like from `M` to `N` and an instance of `MonoidHomClass` (meaning it preserves the monoid structure), a function `f : F`, and a set `s` of type `M`, the image under the function `f` of the submonoid generated by the set `s` is equal to the submonoid generated by the image of the set `s` under the function `f`. In mathematical notation, this means that for a monoid homomorphism `f` and a subset `s` of a monoid, the image of the submonoid generated by `s` under `f` is the same as the submonoid generated by the image of `s` under `f`.
More concisely: For any monoid homomorphism `f` between monoids `M` and `N`, the image of the submonoid generated by `s` in `M` under `f` is equal to the submonoid generated by the image of `s` in `N`.
|
MonoidHom.mrange_eq_map
theorem MonoidHom.mrange_eq_map :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F), MonoidHom.mrange f = Submonoid.map f ⊤
The theorem `MonoidHom.mrange_eq_map` states that for any given types `M` and `N` each equipped with a `MulOneClass` structure (a data type that has both multiplication and a multiplicative identity), a type `F` that is `FunLike` (functions from `M` to `N`), and `MonoidHomClass` (the class of multiplication-preserving functions from `M` to `N`), the range of any monoid homomorphism `f` of type `F` is equal to the image of the entire submonoid of `M` under this homomorphism `f`. Intuitively, this means that every element in the range of a monoid homomorphism `f` is the output of `f` when applied to some element of `M`, and vice versa.
More concisely: For any types `M` and `N` with `MulOneClass`, any `FunLike` type `F` to `N`, and any `MonoidHomClass` function `f : F`, the range of `f` equals the image of the submonoid of `M` under `f`.
|
Submonoid.pow_mem
theorem Submonoid.pow_mem :
∀ {M : Type u_5} [inst : Monoid M] (S : Submonoid M) {x : M}, x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
This theorem states that for any given type `M` equipped with a monoid structure, any submonoid `S` of `M`, and any element `x` from `M` that belongs to `S`, the result of raising `x` to the power of any natural number `n` will also belong to `S`. In mathematical terms, if `S` is a submonoid of a monoid `M`, and `x` is some element of `S`, then `x^n` for any natural number `n` is also an element of `S`.
More concisely: If `S` is a submonoid of the monoid `M`, then for all `x ∈ S` and natural number `n`, `x^n ∈ S`.
|
AddMonoidHom.mrange_top_iff_surjective
theorem AddMonoidHom.mrange_top_iff_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
The theorem `AddMonoidHom.mrange_top_iff_surjective` states that for any types `M` and `N` that are instances of the `AddZeroClass`, any type `F` that is a `FunLike` from `M` to `N` and belongs to `AddMonoidHomClass`, and any function `f` of type `F`, the range of the monoid homomorphism `f` is equal to the entire set (denoted by `⊤`) if and only if the function `f` is surjective. In other words, a monoid homomorphism from `M` to `N` covers the entire target set `N` if and only if for every element in the target set `N`, there exists an element in the source set `M` that `f` maps to it.
More concisely: A monoid homomorphism between additive structures is surjective if and only if its range is the entire target set.
|
Submonoid.coe_one
theorem Submonoid.coe_one : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), ↑1 = 1
This theorem, `Submonoid.coe_one`, states that for any given type `M` that is an instance of the `MulOneClass` (i.e., a type with multiplication and a multiplicative identity element), and for any submonoid `S` of `M`, the multiplicative identity element of the submonoid, when lifted (or coerced) to the type `M`, remains the multiplicative identity. In other words, coercing the identity element `1` of the submonoid `S` to the type `M` gives back the identity element `1` of `M`.
More concisely: For any submonoid `S` of a type `M` with multiplicative identity `1` as an instance of `MulOneClass`, the lifted (or coerced) identity element `1` of `S` is equal to the identity element `1` of `M`.
|
AddSubmonoid.map_sup
theorem AddSubmonoid.map_sup :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (S T : AddSubmonoid M) (f : F),
AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T
The theorem `AddSubmonoid.map_sup` states that for any types `M` and `N`, which are assumed to be additive monoids (as indicated by `[inst : AddZeroClass M]` and `[inst_1 : AddZeroClass N]`), for any type `F` that behaves like a function from `M` to `N` (expressed by `[inst_2 : FunLike F M N]`) and is a homomorphism between additive monoids (`[mc : AddMonoidHomClass F M N]`), for any additive submonoids `S` and `T` of `M`, and for any function `f` of type `F`, the image of the supremum (join) of `S` and `T` under `f` is the same as the supremum of the image of `S` under `f` and the image of `T` under `f`. In simpler terms, mapping the join of two submonoids is the same as joining the maps of the two submonoids.
More concisely: For additive monoids M and N, homomorphism F : M -> N, and additive submonoids S and T of M, the image of the join (supremum) of S and T under F is equal to the join of the images of S and T under F.
|
SubmonoidClass.coe_pow
theorem SubmonoidClass.coe_pow :
∀ {M : Type u_6} [inst : Monoid M] {A : Type u_5} [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] {S : A}
(x : ↥S) (n : ℕ), ↑(x ^ n) = ↑x ^ n
This theorem, `SubmonoidClass.coe_pow`, states that for any type `M` with a monoid structure, any type `A` that behaves like a set of `M` with a submonoid class, any specific submonoid `S` of `A`, and any element `x` from `S`, the operation of raising `x` to the power of a natural number `n` (denoted `x ^ n`), and then taking the coercion of the result to `M` (denoted `↑(x ^ n)`), is equal to first taking the coercion of `x` to `M` and then raising the result to the power of `n` (denoted `↑x ^ n`). This essentially states the compatibility of the power operation with the coercion from the submonoid to the monoid.
More concisely: For any monoid `M`, submonoid `S` of a type `A` with the submonoid structure, and `x` in `S`, the coercion of `x^n` to `M` equals the coercion of `x` to `M` raised to the power of `n`.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.20
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.20 :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F) {x : M}, (x ∈ MonoidHom.mker f) = (f x = 1)
This theorem states that for any types `M`, `N`, and `F`, if `M` and `N` have multiplicative and identity structure (expressed as `MulOneClass M` and `MulOneClass N`), `F` is function-like from `M` to `N` (expressed as `FunLike F M N`), and `F` is a monoid homomorphism class from `M` to `N` (expressed as `MonoidHomClass F M N`), then for any function `f` of type `F` and any element `x` of type `M`, `x` is in the multiplicative kernel (or mker) of `f` if and only if the function `f` applied to `x` equals the multiplicative identity, which in this context is `1`.
In mathematical terms, if `f: M → N` is a monoid homomorphism, the multiplicative kernel of `f` (denoted `MonoidHom.mker f` in Lean and usually `ker f` in mathematical notation) is the set of all elements `x` in `M` such that `f(x) = 1`, where `1` is the identity element of the monoid `N`. The theorem states that `x` belongs to the kernel of `f` if and only if `f(x) = 1`.
More concisely: For any monoid homomorphisms `f: M → N` between multiplicative monoids `M` and `N`, the element `x` in `M` belongs to the multiplicative kernel of `f` if and only if `f(x) = 1`.
|
AddMonoidHom.mrange_eq_map
theorem AddMonoidHom.mrange_eq_map :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddMonoidHom.mrange f = AddSubmonoid.map f ⊤
The theorem `AddMonoidHom.mrange_eq_map` states that for any types `M`, `N`, and `F`, where `M` and `N` have the structure of add-zero classes, `F` behaves like a function from `M` to `N` and `F` is an additive monoid homomorphism, then for any instance `f` of `F`, the range of `f` (considered as an additive monoid homomorphism) is equal to the image of the entire additive submonoid of `M` under `f`. In simpler terms, this theorem says that the set of all outputs of `f` is the same as the set of all values `f` can produce when applied to all elements of `M`.
More concisely: For any additive monoid homomorphism `f` from an add-zero class `M` to an add-zero class `N`, the image of the submonoid generated by `M` under `f` equals the range of `f`.
|
AddMonoidHom.map_mclosure
theorem AddMonoidHom.map_mclosure :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (s : Set M),
AddSubmonoid.map f (AddSubmonoid.closure s) = AddSubmonoid.closure (⇑f '' s)
This theorem states that for any set `s` in an additive monoid `M`, and any homomorphism `f` from `M` to another additive monoid `N`, the additive submonoid generated by the image of `s` under `f` (denoted by `⇑f '' s`) is the same as the image under `f` of the additive submonoid generated by `s`. In other words, mapping a set to another monoid and then taking the generated submonoid yields the same result as first taking the generated submonoid and then mapping it to the other monoid. This means the operations of "taking the generated submonoid" and "mapping with `f`" commute with each other.
More concisely: For any set `s` in an additive monoid `M` and any homomorphism `f` from `M` to an additive monoid `N`, the image of the additive submonoid generated by `s` under `f` equals the additive submonoid generated by the image of `s` under `f`.
|
AddSubmonoid.map_le_iff_le_comap
theorem AddSubmonoid.map_le_iff_le_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N},
AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T
This theorem establishes a key property regarding the relationship between `map` and `comap` operations on `AddSubmonoid`s under add monoid homomorphisms. Specifically, for any types `M` and `N` that are additive monoids, any function `f` from `M` to `N` that is an additive monoid homomorphism, and any `AddSubmonoid`s `S` of `M` and `T` of `N`, the image of `S` under `f` is a submonoid of `T` if and only if `S` is a submonoid of the preimage of `T` under `f`. This means that the mapping of `S` to `N` through `f` is contained in `T` exactly when `S` is contained in the set of elements in `M` that map to `T` via `f`.
More concisely: For any additive monoid homomorphisms f between additive monoids M and N, and any AddSubmonoids S of M and T of N, the image of S under f is a submonoid of T if and only if S is a submonoid of the preimage of T under f.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.2
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.2 :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M},
(x ∈ AddSubmonoid.comap f S) = (f x ∈ S)
The theorem `Mathlib.GroupTheory.Submonoid.Operations._auxLemma.2` states that for any types `M` and `N` with `AddZeroClass` instances (meaning they have additive structures with a zero element), a type `F` which has `FunLike` and `AddMonoidHomClass` instances (meaning it can behave like a function and is a homomorphism between additive monoids), an additive submonoid `S` of `N`, a function `f` of type `F`, and an element `x` of `M`, an element `x` belongs to the preimage of the submonoid `S` under the function `f` if and only if the function `f` applied to `x` belongs to `S`.
In mathematical terms, it basically says that the preimage of a submonoid under a function is indeed a submonoid.
More concisely: The preimage of an additive submonoid under a homomorphism is a submonoid.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.8
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.8 :
∀ {A : Type u_4} {M₁ : Type u_5} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] {S' : A}
{x : ↥S'}, (↑x = 0) = (x = 0)
This theorem states that for any type `A`, any `M₁` of type `A`, given that `A` acts like a set on `M₁`, `M₁` has a zero element, and `A` contains the zero of `M₁`, and for any `S'` of type `A` and any `x` that belongs to `S'`, the proposition that `x` is equal to `0` when upcast from `S'` to `M₁` is equivalent to the proposition that `x` equals `0` within `S'`. In other words, the zero element in the subtype `S'` is the same as the zero element in the supertype `M₁` when `x` is an element of `S'`.
More concisely: For any type `A` with a zero element `0`, and for any subtype `S` of `A` with the same zero element, any element `x` in `S` equals `0` in `S` if and only if it equals `0` in `A`.
|
MonoidHom.coe_mrange
theorem MonoidHom.coe_mrange :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F), ↑(MonoidHom.mrange f) = Set.range ⇑f
The theorem `MonoidHom.coe_mrange` states that for any given monoid homomorphism `f` of type `F`, where `F` is a function-like object from a monoid `M` to another monoid `N`, the coimage of the range of `f` under the natural embedding from a submonoid of `N` into `N` itself, is equal to the set of images of `f`. In other words, it asserts that the set of all the values we can get by applying the monoid homomorphism to elements of 'M' is exactly the same as the range of the function `f`.
More concisely: The coimage of the range of a monoid homomorphism under the natural embedding is equal to the image of the homomorphism.
|
Submonoid.bot_or_exists_ne_one
theorem Submonoid.bot_or_exists_ne_one :
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ∨ ∃ x ∈ S, x ≠ 1
This theorem states that for any type `M` that is an instance of `MulOneClass` (i.e., it has a multiplication operation and a distinguished "one" element that serves as the identity for multiplication), and for any submonoid `S` of `M`, `S` is either the trivial submonoid (denoted `⊥`) or there exists an element `x` in `S` that is not equal to the identity element `1`. In other words, every submonoid is either trivial or contains at least one element that isn't the multiplicative identity.
More concisely: Every submonoid of a `MulOneClass` type `M` is either the trivial submonoid or contains an element distinct from the multiplicative identity.
|
AddMonoidHom.coe_mrange
theorem AddMonoidHom.coe_mrange :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), ↑(AddMonoidHom.mrange f) = Set.range ⇑f
The theorem `AddMonoidHom.coe_mrange` states that for any types `M`, `N`, and `F`, with `M` and `N` being additive monoids (i.e., they contain a zero and an addition operation), and `F` being a function-like object from `M` to `N`, the range of a homomorphism `f : F` (which preserves the addition operation and the zero) is equal to the set of all images of elements in `M` under `f`. In other words, the range of `f` as an additive monoid homomorphism is the same as the range of `f` as a function.
More concisely: The range of an additive monoid homomorphism from one additive monoid to another as a set equals the images of its elements under the homomorphism.
|
Submonoid.le_comap_of_map_le
theorem Submonoid.le_comap_of_map_le :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F},
Submonoid.map f S ≤ T → S ≤ Submonoid.comap f T
The theorem `Submonoid.le_comap_of_map_le` states that for all types `M` and `N` with multiplication and identity (`MulOneClass M` and `MulOneClass N`), a submonoid `S` of `M`, a function `f` of type `F` that behaves like a function from `M` to `N` (`FunLike F M N`), and is a monoid homomorphism (`MonoidHomClass F M N`), and a submonoid `T` of `N`. If the image of submonoid `S` under the function `f` is a subset or equal to the submonoid `T`, then `S` is a subset or equal to the preimage of `T` under the function `f`.
More concisely: If `f` is a monoid homomorphism from a submonoid `S` of `M` to a submonoid `T` of `N` such that `f(S) ⊆ T`, then `S ⊆ f⁻¹(T)`.
|
Submonoid.eq_bot_iff_forall
theorem Submonoid.eq_bot_iff_forall :
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ↔ ∀ x ∈ S, x = 1
This theorem states that for any type `M` having a multiplicative identity (i.e., an instance of `MulOneClass`), a submonoid `S` is equal to the trivial submonoid (denoted as `⊥` in Lean) if and only if all elements `x` in `S` are equal to the multiplicative identity (`1`). In other words, a submonoid is trivial if it contains only the multiplicative identity element.
More concisely: A submonoid of a type with a multiplicative identity is the trivial submonoid if and only if all its elements equal the multiplicative identity.
|
Submonoid.bot_or_nontrivial
theorem Submonoid.bot_or_nontrivial :
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), S = ⊥ ∨ Nontrivial ↥S
This theorem states that for any given submonoid `S` of a certain type `M`, which is a multiplicative monoid (a set equipped with an associative binary operation and an identity element), `S` is either the bottom element (the trivial submonoid typically consisting only of the identity element), or it is nontrivial. In other words, any submonoid is either trivial or contains at least two distinct elements.
More concisely: Any submonoid of a multiplicative monoid is either the trivial submonoid with only the identity element, or it contains at least two distinct elements.
|
ZeroMemClass.coe_eq_zero
theorem ZeroMemClass.coe_eq_zero :
∀ {A : Type u_4} {M₁ : Type u_5} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] {S' : A}
{x : ↥S'}, ↑x = 0 ↔ x = 0
This theorem states that for any type `A` and `M₁`, given that `A` behaves like a set of `M₁`, `M₁` has a zero element, and `A` belongs to the `ZeroMemClass` of `M₁`, for any element `S'` of `A` and any element `x` within `S'`, the condition of `x` being equal to zero is equivalent to the embedding of `x` (denoted by `↑x`) being zero. In other words, an element of a subset of `A` is zero if and only if its embedding in `M₁` is also zero.
More concisely: For any type `A` and `M₁` such that `A` is a set-like structure over `M₁`, `M₁` has a zero element, and `A` is in the zero-membership class of `M₁`, the embedding of an element `x` in `A` is zero if and only if `x` is zero in `A`.
|
ZeroMemClass.coe_zero
theorem ZeroMemClass.coe_zero :
∀ {A : Type u_4} {M₁ : Type u_5} [inst : SetLike A M₁] [inst_1 : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A),
↑0 = 0
This theorem, `ZeroMemClass.coe_zero`, states that for any type `A` and `M₁`, given that `A` has a `SetLike` instance, `M₁` has a `Zero` instance, and there exists a `ZeroMemClass` instance between `A` and `M₁`, if `S'` is an element of `A`, then the coercion of `0` to `M₁` is equal to `0`. In simpler terms, it means that zero remains zero after being transformed from one type to another under the provided conditions.
More concisely: For any type `A` with a `SetLike` instance, any type `M₁` with a `Zero` instance, and given a `ZeroMemClass` instance between `A` and `M₁`, the coercion of `0` from `M₁` is equal to the zero element of `A`.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.3
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.3 :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N},
(y ∈ Submonoid.map f S) = ∃ x ∈ S, f x = y
This theorem states that for any given types `M`, `N` and `F`, where `M` and `N` are equipped with the structure of `MulOneClass` (which essentially means they have multiplicative identities and multiplication operations), `F` is "function-like" from `M` to `N`, and `F` has the structure of a `MonoidHomClass` (which makes `F` a monoid homomorphism from `M` to `N`). Given a function `f` of type `F` and a submonoid `S` of `M`, for any element `y` of `N`, `y` is in the image of `S` under `f` if and only if there exists an element `x` in `S` such that `f(x)` equals `y`. In mathematical terms, it asserts that $y \in f(S)$ if and only if there exists $x \in S$ such that $f(x) = y$.
More concisely: For any monoid homomorphism `F` from a multiplicative monoid `M` to a multiplicative monoid `N` and any submonoid `S` of `M`, the image of `S` under `F` equals the set of elements in `N` that have preimages in `S`.
|
AddSubmonoid.eq_top_iff'
theorem AddSubmonoid.eq_top_iff' :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊤ ↔ ∀ (x : M), x ∈ S
This theorem states that for any type `M` that has an addition and zero operation (i.e., an "AddZeroClass"), and for any additive submonoid `S` of `M`, `S` is equal to the top element (which represents the whole set in this context) if and only if every element `x` of type `M` is in `S`. In other words, an additive submonoid of `M` is the whole of `M` if and only if every element in `M` is also in the submonoid.
More concisely: An additive submonoid of a type `M` with addition and zero is equal to the whole `M` if and only if every element of `M` is in the submonoid.
|
Submonoid.smul_def
theorem Submonoid.smul_def :
∀ {M' : Type u_5} {α : Type u_6} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α),
g • a = ↑g • a
This theorem, `Submonoid.smul_def`, states that for any type 'M' that forms a multiplicative group with an identity element (which we signify with `MulOneClass M'`) and any type 'α' that can be scaled by elements of type 'M' (which we capture with `SMul M' α`), if we have a submonoid 'S' of 'M' and an element 'g' of that submonoid, the scalar multiplication of 'g' and an element 'a' of type 'α' is the same as the scalar multiplication of the representative of 'g' (which belongs to 'M') and 'a'. In simpler terms, the theorem states that scalar multiplication behaves the same way in the submonoid as in the parent group.
More concisely: For any submonoid 'S' of a multiplicative group 'M' with identity, and any 'g' in 'S' and 'a' in the type 'α' scalable by 'M', the scalar multiplication of 'g' and 'a' equals the scalar multiplication of any representative of 'g' in 'M' and 'a'.
|
Mathlib.GroupTheory.Submonoid.Operations._auxAddLemma.20
theorem Mathlib.GroupTheory.Submonoid.Operations._auxAddLemma.20 :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) {x : M}, (x ∈ AddMonoidHom.mker f) = (f x = 0)
This theorem, `Mathlib.GroupTheory.Submonoid.Operations._auxAddLemma.20`, states that for every type `M`, `N` and `F` such that `M` and `N` form add-zero classes, `F` is a function-like structure from `M` to `N` and `F` is an additive monoid homomorphism from `M` to `N`, and for every function `f : F` and element `x : M`, `x` belongs to the additive kernel of the homomorphism `f` if and only if `f(x) = 0`. The additive kernel of a homomorphism is the subset of elements that get mapped to the additive identity (zero).
More concisely: For any additive monoid homomorphism `f` from an add-zero class `M` to an add-zero class `N`, `x` in `M` belongs to the kernel of `f` if and only if `f(x) = 0`.
|
Submonoid.map_le_iff_le_comap
theorem Submonoid.map_le_iff_le_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N},
Submonoid.map f S ≤ T ↔ S ≤ Submonoid.comap f T
This theorem, `Submonoid.map_le_iff_le_comap`, states that for any given types `M` and `N` that are instances of `MulOneClass`, any type `F` that is a `FunLike` function from `M` to `N` and a `MonoidHomClass`, and any given submonoids `S` of `M` and `T` of `N`, as well as a function `f` of type `F`, the image of `S` under `f` is a submonoid of `T` if and only if `S` is a submonoid of the preimage of `T` under `f`. In other words, the statement is about the relationship between the image and preimage of submonoids under a monoid homomorphism.
More concisely: For any submonoids S of type M and T of type N, and any monoid homomorphism f : M -> N between types M and N, the image of S under f is a submonoid of T if and only if S is a submonoid of the preimage of T under f.
|
Submonoid.coe_mul
theorem Submonoid.coe_mul : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) (x y : ↥S), ↑(x * y) = ↑x * ↑y
This theorem, `Submonoid.coe_mul`, states that for any type `M` that has a multiplication and a one (captured by the typeclass `MulOneClass M`), and for any submonoid `S` of `M`, the result of multiplying two elements `x` and `y` in the submonoid and then coercing to the parent monoid is the same as first coercing the elements to the parent monoid and then multiplying them. Essentially, it's saying that multiplication in the submonoid is the same as multiplication in the parent monoid when we view the elements as elements of the parent monoid.
More concisely: For any type `M` with multiplication and one, and for any submonoid `S` of `M`, the multiplication of elements in `S` coerced to `M` is equal to the multiplication of the same elements in `M`.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.7
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.7 :
∀ {A : Type u_4} {M₁ : Type u_5} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] {S' : A} {x : ↥S'},
(↑x = 1) = (x = 1)
This theorem pertains to the field of Group Theory, specifically to submonoids. It states that for any type `A`, type `M₁`, where `A` acts like a set and `M₁` has a 'one' entity, and `A` is a class that contains the 'one' of `M₁`, if we have an element `x` of a subset `S'` of `A`, then the statement "the underlying element of `x` is equal to 'one'" is equivalent to the statement "`x` itself is equal to the 'one' of the subset `S'`". This theorem essentially says that the element `1` in the subset is the same as the element `1` in the original set when we consider the elements up to the subset structure.
More concisely: For any set `A` with a 'one' element `1` and submonoid `M₁` containing `1`, the element `x` in `M₁` is equal to the 'one' of `M₁` if and only if the underlying element of `x` in `A` is equal to the 'one' of `A`.
|
AddSubmonoid.bot_or_exists_ne_zero
theorem AddSubmonoid.bot_or_exists_ne_zero :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ∨ ∃ x ∈ S, x ≠ 0
This theorem states that for any type `M` that is an instance of the `AddZeroClass`, any additive submonoid `S` of `M` is either the trivial additive submonoid or contains a non-zero element. In other words, every additive submonoid is either the submonoid containing only the zero element, or there exists an element in that submonoid which is not zero.
More concisely: Every non-trivial additive submonoid of an AddZeroClass type contains a non-zero element.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.4
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.4 :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N},
(y ∈ AddSubmonoid.map f S) = ∃ x ∈ S, f x = y
This theorem states that for any types `M`, `N`, and `F`, where `M` and `N` are equipped with `AddZeroClass` structures (i.e., they are additive monoids with a zero element), `F` is a function type from `M` to `N` (`FunLike F M N`) and is also an additive monoid homomorphism (`AddMonoidHomClass F M N`), given any function `f` of type `F` and a submonoid `S` of `M`, and any element `y` of `N`, `y` is in the image of `S` under `f` (i.e., `y` is in `AddSubmonoid.map f S`) if and only if there exists an element `x` in `S` such that `f` applied to `x` equals `y` (written as `f x = y`). In mathematical terms, this theorem characterizes the image of an additive submonoid under an additive monoid homomorphism.
More concisely: For any additive monoids M, N, and an additive monoid homomorphism F from M to N, an element y of N belongs to the image of an additive submonoid S of M under F if and only if there exists an element x in S such that F(x) = y.
|
Mathlib.GroupTheory.Submonoid.Operations._auxLemma.1
theorem Mathlib.GroupTheory.Submonoid.Operations._auxLemma.1 :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M},
(x ∈ Submonoid.comap f S) = (f x ∈ S)
This theorem states that for any types `M`, `N`, and `F` and for any instances of `MulOneClass` on `M` and `N`, any instance of `FunLike` from `F` to a function from `M` to `N`, and any instance of `MonoidHomClass` on `F`, `M` and `N`, if `S` is a submonoid of `N` and `f` is a function of type `F`, then for any element `x` of `M`, `x` belongs to the preimage of the submonoid `S` along the monoid homomorphism `f` if and only if `f(x)` belongs to `S`. In simpler terms, it means that an element is in the preimage submonoid under a homomorphism if its image under the homomorphism is in the original submonoid.
More concisely: For any monoid homomorphisms between types `M`, `N`, and `F` with `MulOneClass` and `MonoidHomClass` instances, an element `x` in `M` is in the preimage of submonoid `S` in `N` under `f` if and only if `f(x)` belongs to `S`.
|
Submonoid.gc_map_comap
theorem Submonoid.gc_map_comap :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F),
GaloisConnection (Submonoid.map f) (Submonoid.comap f)
The theorem `Submonoid.gc_map_comap` states that for any types `M` and `N` that are instances of the `MulOneClass` (i.e., they carry binary multiplication and a one element), and any type `F` that is an instance of `FunLike F M N` and `MonoidHomClass F M N` (meaning `F` acts like a monoid homomorphism from `M` to `N`), then for any element `f : F`, there exists a Galois connection between the function `Submonoid.map f` and the function `Submonoid.comap f`. In other words, for any submonoid in `M`, mapping it to `N` through `f` and then taking the preimage back to `M` is an operation that is less than or equal to the original submonoid. Similarly, for any submonoid in `N`, taking its preimage in `M` through `f` and then mapping it back to `N` is an operation greater than or equal to the original submonoid.
More concisely: For any instances `M` of `MulOneClass`, `N` of `MulOneClass`, `F` of `FunLike F M N` and `MonoidHomClass F M N`, the maps `Submonoid.map f : Submonoid M -> Submonoid N` and `Submonoid.comap f : Submonoid N -> Submonoid M` form a Galois connection.
|
AddMonoidHom.mrange_top_of_surjective
theorem AddMonoidHom.mrange_top_of_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F),
Function.Surjective ⇑f → AddMonoidHom.mrange f = ⊤
The theorem `AddMonoidHom.mrange_top_of_surjective` states that for any given types `M` and `N` that have `AddZeroClass` instances, and for any type `F` that is function-like from `M` to `N` and has an `AddMonoidHomClass` instance, if a function `f` of type `F` is surjective, meaning that every element of `N` is the image of some element of `M` under `f`, then the range of the `AddMonoid` homomorphism `f` is the entire codomain, `N`. In other words, every element of `N` is the result of the additive monoid homomorphism `f` applied to some element of `M`.
More concisely: If `F` is a surjective additive monoid homomorphism from the additive monoid of type `M` to the additive monoid of type `N`, then the range of `F` is the entire codomain `N`.
|
Submonoid.le_comap_map
theorem Submonoid.le_comap_map :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (S : Submonoid M) {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F}, S ≤ Submonoid.comap f (Submonoid.map f S)
The theorem `Submonoid.le_comap_map` states that for any submonoid `S` in a given `MulOneClass` `M`, and any function `f` of type `F` that is a monoid homomorphism from `M` to another `MulOneClass` `N` (as ensured by `FunLike F M N` and `MonoidHomClass F M N`), the submonoid `S` is a subset (or equal to) the preimage under `f` of the image of `S` under `f`. In other words, application of the function `f` to the submonoid `S` followed by taking the preimage under `f` does not remove any elements from `S`. The theorem encapsulates a fundamental property of submonoids under homomorphic images and their preimages.
More concisely: For any submonoid S of a MulOneClass M and any monoid homomorphism f from M to another MulOneClass N, the image of S under f is contained in the preimage of f(S) under f.
|
OneMemClass.coe_one
theorem OneMemClass.coe_one :
∀ {A : Type u_4} {M₁ : Type u_5} [inst : SetLike A M₁] [inst_1 : One M₁] [hA : OneMemClass A M₁] (S' : A), ↑1 = 1
This theorem, `OneMemClass.coe_one`, asserts that for any types `A` and `M₁`, if `A` behaves like a set of `M₁`, and `M₁` has an identity element under a certain operation, and there exists a class `OneMemClass` such that the number 1 is in this class, then the identity element is 1 when coe-function is applied on 1. In essence, it's stating that if we coerce the number 1 (in the context of a certain class and type conditions), it will remain 1.
More concisely: If `A` is a set-like type, `M₁` has an identity element `e` for some operation, and `1` is in class `OneMemClass`, then `coe (1 : M₁) = e`.
|
Submonoid.map_sup
theorem Submonoid.map_sup :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F),
Submonoid.map f (S ⊔ T) = Submonoid.map f S ⊔ Submonoid.map f T
The theorem `Submonoid.map_sup` states that for any two submonoids `S` and `T` of a MulOneClass `M`, and a monoid homomorphism `f` from `M` to another MulOneClass `N`, the image of the join (supremum) of `S` and `T` under `f` is the same as the join (supremum) of the images of `S` and `T` under `f`. Essentially, this says that the mapping `f` preserves the join operation in the submonoid structure, which is an important property for morphisms in algebra.
More concisely: For any submonoids S and T of a MulOneClass M and any monoid homomorphism f from M to another MulOneClass N, the image of the supremum of S and T under f is equal to the supremum of the images of S and T under f.
|
MonoidHom.mrange_top_iff_surjective
theorem MonoidHom.mrange_top_iff_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] {f : F}, MonoidHom.mrange f = ⊤ ↔ Function.Surjective ⇑f
The theorem `MonoidHom.mrange_top_iff_surjective` states that for any given types `M` and `N` - assumed to be instances of `MulOneClass` (that is, they have multiplicative identity) - and any function type `F` which is a `FunLike` from `M` to `N` and also a `MonoidHomClass` from `M` to `N`, for any function `f` of type `F`, the monoid homomorphism range of `f` is the entire codomain (`⊤`) if and only if `f` is a surjective function. In other words, a function `f` between two monoids is surjective if it maps to every element in the codomain.
More concisely: A function between two monoids is a surjection if and only if its monoid homomorphism range equals the codomain.
|
AddSubmonoid.bot_or_nontrivial
theorem AddSubmonoid.bot_or_nontrivial :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ∨ Nontrivial ↥S
This theorem states that for any type `M` that is an instance of the `AddZeroClass` class (meaning it has an addition operation and a zero element), any additive submonoid `S` of `M` is either the trivial additive submonoid (denoted ⊥), or it is nontrivial. In other words, an additive submonoid of `M` is always either the trivial submonoid containing only the zero element, or it contains at least two distinct elements.
More concisely: Every additive submonoid of a type `M` with addition and zero element is either the trivial submonoid consisting only of the zero element or a nontrivial submonoid containing at least two distinct elements.
|
MonoidHom.mrange_top_of_surjective
theorem MonoidHom.mrange_top_of_surjective :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_5}
[inst_2 : FunLike F M N] [mc : MonoidHomClass F M N] (f : F), Function.Surjective ⇑f → MonoidHom.mrange f = ⊤
The theorem `MonoidHom.mrange_top_of_surjective` states that for any two types `M` and `N` with `MulOneClass` instances (i.e., they have multiplicative identity and multiplication defined), and for any type `F` which has a `FunLike` instance from `M` to `N`, and `MonoidHomClass` instance, if `f` is a function from `F`, and the function is surjective (meaning that for every element of `N` there's an element of `M` such that `f` of that element equals the given element), then the range of the monoid homomorphism `f` is the entire codomain `N`. In other words, `f` maps `M` onto `N` under the monoid operation.
More concisely: If `M` and `N` are types with multiplicative identities and `F:` `M` → `N` is a surjective monoid homomorphism, then the range of `F` is the entire codomain `N` under the monoid operation.
|
AddSubmonoid.eq_bot_iff_forall
theorem AddSubmonoid.eq_bot_iff_forall :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ↔ ∀ x ∈ S, x = 0
The theorem `AddSubmonoid.eq_bot_iff_forall` states that for any type `M` that has an addition operation and a zero element (i.e., for any `M` that is an instance of the `AddZeroClass`), a given additive submonoid `S` of `M` is equal to the bottom element (which represents the trivial submonoid containing only the zero element) if and only if every element `x` in `S` is equal to zero.
More concisely: For any additive submonoid `S` of an additive semigroup `M` with zero element, `S` equals the bottom submonoid if and only if every element in `S` is equal to the zero element.
|