Mathlib.GroupTheory.Submonoid.Basic._auxLemma.2
theorem Mathlib.GroupTheory.Submonoid.Basic._auxLemma.2 :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {x : M}, (x ∈ s.toAddSubsemigroup) = (x ∈ s) := by
sorry
This theorem states that for any type `M` that forms an `AddZeroClass`, for any additive submonoid `s` of `M`, and for any element `x` of `M`, `x` being an element of the additive subsemigroup associated with `s` is equivalent to `x` being an element of `s` itself. In other words, the membership of `x` in the additive subsemigroup derived from the submonoid is the same as its membership in the original submonoid.
More concisely: For any AddZeroClass type M, any additive submonoid s of M, and any x in M, x belongs to the additive subsemigroup of s if and only if x belongs to s.
|
Submonoid.closure_le
theorem Submonoid.closure_le :
∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {S : Submonoid M}, Submonoid.closure s ≤ S ↔ s ⊆ ↑S
The theorem `Submonoid.closure_le` states that for any type `M` equipped with a `MulOneClass` structure (that is, a multiplication operation and a multiplicative identity), any set `s` of elements of type `M`, and any submonoid `S` of `M`, the submonoid generated by `s` (denoted as `Submonoid.closure s`) is a subset of `S` if and only if the set `s` itself is a subset of the underlying set of `S` (denoted as `↑S`). In other words, a submonoid `S` contains the submonoid generated by a set `s` if and only if it contains all the elements of `s`.
More concisely: A submonoid contains the submonoid generated by a set if and only if the set is a subset of the submonoid.
|
AddSubmonoid.coe_iInf
theorem AddSubmonoid.coe_iInf :
∀ {M : Type u_1} [inst : AddZeroClass M] {ι : Sort u_4} {S : ι → AddSubmonoid M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i) := by
sorry
This theorem states that for any given type `M` with an additive zero structure and for any indexing type `ι`, for a family of additive submonoids `S` indexed by `ι`, the coercion of the greatest lower bound (infimum) of the submonoids `S` is equal to the intersection of the individual coercions of the submonoids `S`. In simpler terms, the elements of the smallest submonoid containing all the submonoids `S` are exactly the elements that belong to every submonoid in the collection `S`.
More concisely: For any additive type `M` with zero structure and indexing type `ι`, the infimum of a family `S` of its additive submonoids equals the intersection of the submonoids' coercions.
|
Submonoid.closure_eq
theorem Submonoid.closure_eq : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), Submonoid.closure ↑S = S := by
sorry
The theorem `Submonoid.closure_eq` asserts that for any type `M` equipped with a multiplicative identity and a multiplication operation (the `MulOneClass M` instance), and any submonoid `S` of `M`, the closure of `S` (i.e., the smallest submonoid of `M` that contains `S`) is equal to `S` itself. This means that the submonoid `S` is already closed under the operations of the `MulOneClass`, and no additional elements from `M` are needed to complete it.
More concisely: For any submonoid `S` of a multiplicative monoid `M`, the submonoid generated by `S` (i.e., the smallest submonoid containing `S`) is equal to `S` itself.
|
AddSubmonoid.mem_top
theorem AddSubmonoid.mem_top : ∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), x ∈ ⊤
This theorem states that for any type `M` that has the structure of an additive monoid with zero (i.e., it has an operation of addition that is associative, a zero element that serves as an identity for addition, and every element has an additive inverse), every element `x` of `M` is an element of the top element (`⊤`) of the lattice of submonoids of `M`. In the context of lattice theory, the top element of a lattice is the greatest element that is greater than or equal to every other element in the lattice.
More concisely: Every additive monoid with zero has the property that every element is contained in the top element of its lattice of submonoids.
|
Submonoid.mem_closure
theorem Submonoid.mem_closure :
∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {x : M},
x ∈ Submonoid.closure s ↔ ∀ (S : Submonoid M), s ⊆ ↑S → x ∈ S
The theorem `Submonoid.mem_closure` states that for any type `M` that has a multiplication and one (`MulOneClass`), any set `s` of `M`, and any element `x` of `M`, the element `x` is in the submonoid generated by the set `s` if and only if for every submonoid `S` of `M`, if `s` is a subset of the carrier of `S` (`↑S`), then `x` is an element of `S`. In simpler terms, it means that an element is in the smallest submonoid containing a set if and only if it is in every submonoid that contains the set.
More concisely: An element is in the smallest submonoid generated by a set if and only if it belongs to every submonoid containing that set.
|
Submonoid.one_mem'
theorem Submonoid.one_mem' : ∀ {M : Type u_4} [inst : MulOneClass M] (self : Submonoid M), 1 ∈ self.carrier
This theorem states that for any given submonoid `self` of a type `M` that forms a multiplicative monoid, the multiplicative identity `1` is an element of the `carrier` set of `self`. In other words, the number `1` is always a member of any submonoid in a multiplication-based structure.
More concisely: In any multiplicative submonoid of a type, the multiplicative identity 1 is an element.
|
AddSubmonoid.zero_mem
theorem AddSubmonoid.zero_mem : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), 0 ∈ S
This theorem states that for any `AddSubmonoid` `S` of a type `M`, which is an instance of the `AddZeroClass`, the additive identity element `0` is a member of `S`. In other words, the set `S` always includes the element 0. Here, `AddZeroClass` is a class that combines addition and a zero element in the context of algebraic structures.
More concisely: For any AddSubmonoid S of type M that is an instance of AddZeroClass, the additive identity 0 is an element of S.
|
Submonoid.mem_bot
theorem Submonoid.mem_bot : ∀ {M : Type u_1} [inst : MulOneClass M] {x : M}, x ∈ ⊥ ↔ x = 1
This theorem states that for any type `M` equipped with the structure of a `MulOneClass` (a structure containing multiplication and a multiplicative identity, which is `1`), a certain element `x` belongs to the smallest submonoid (denoted as `⊥`) if and only if `x` is equal to the multiplicative identity (`1`). In other words, the smallest submonoid of a `MulOneClass` is simply the set containing the multiplicative identity.
More concisely: In a `MulOneClass` type, the smallest submonoid equals the set of multiplicative identities.
|
Submonoid.one_mem
theorem Submonoid.one_mem : ∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M), 1 ∈ S
This theorem states that for any given submonoid `S` of a type `M` that forms a `MulOneClass` (a multiplicative monoid with a multiplicative identity, or `1`), the multiplicative identity (`1`) is an element of `S`. In other words, in the context of abstract algebra, this theorem says that the identity element of a monoid is also an element of any of its submonoids.
More concisely: In any multiplicative monoid with identity, the identity is an element of every submonoid.
|
Submonoid.ext
theorem Submonoid.ext :
∀ {M : Type u_1} [inst : MulOneClass M] {S T : Submonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
This theorem states that for any given type `M` that has a multiplication and identity operation (i.e., `M` is a mul-one-class), two submonoids `S` and `T` of `M` are equal if every element `x` of `M` belongs to `S` if and only if `x` belongs to `T`. In other words, if the same elements from `M` belong to both `S` and `T`, then `S` and `T` are considered the same submonoid.
More concisely: Two submonoids of a type `M` with multiplication and identity operations are equal if and only if they contain the same elements of `M`.
|
MonoidHom.eqOn_closureM
theorem MonoidHom.eqOn_closureM :
∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {f g : M →* N} {s : Set M},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(Submonoid.closure s)
This theorem states that if two monoid homomorphisms, represented by the functions `f` and `g`, are equal on a set `s` of elements of a monoid `M`, then these homomorphisms are also equal on the submonoid closure of this set. Here, a monoid is a type `M` equipped with an associative multiplication operation and an identity element, and a monoid homomorphism is a function that preserves the multiplication operation and the identity element. The submonoid closure of a set is the smallest submonoid that contains this set, and the condition that two functions are equal on a set means that their values coincide for each element of this set.
More concisely: If two monoid homomorphisms agree on a set, they agree on its submonoid closure.
|
Mathlib.GroupTheory.Submonoid.Basic._auxLemma.9
theorem Mathlib.GroupTheory.Submonoid.Basic._auxLemma.9 :
∀ {M : Type u_1} [inst : AddZeroClass M] {x : M}, (x ∈ ⊥) = (x = 0)
This theorem from the Mathlib Group Theory Submonoid Basic states that for any type `M` which has an `AddZeroClass` instance (which means it has addition and zero elements), for any element `x` of `M`, `x` belongs to the bottom submonoid (`⊥`) if and only if `x` is the zero element. Here, `⊥` represents the trivial submonoid consisting only of the zero element. This theorem is essentially saying that the only element in the trivial submonoid is zero.
More concisely: For any additive type M, an element x belongs to the trivial submonoid if and only if x is the additive zero.
|
AddMonoidHom.eqOn_closureM
theorem AddMonoidHom.eqOn_closureM :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {f g : M →+ N} {s : Set M},
Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubmonoid.closure s)
The theorem `AddMonoidHom.eqOn_closureM` asserts the following: For any types `M` and `N` that have an addition and a zero (`AddZeroClass`), any two additive monoid homomorphisms `f` and `g` from `M` to `N`, and any set `s` of type `M`, if `f` and `g` are equal on the set `s` (i.e., they map every element of `s` to the same element in `N`), then they are also equal on the additive submonoid generated by this set `s` (that is, they map every element of this submonoid to the same element in `N`). In other words, the equality of two monoid homomorphisms on a set extends to the closure of the set under the monoid operation.
More concisely: If two additive monoid homomorphisms from an `AddZeroClass` type agree on a set, they agree on the submonoid generated by that set.
|
AddSubmonoid.closure_induction'
theorem AddSubmonoid.closure_induction' :
∀ {M : Type u_1} [inst : AddZeroClass M] (s : Set M) {p : (x : M) → x ∈ AddSubmonoid.closure s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
p 0 ⋯ →
(∀ (x : M) (hx : x ∈ AddSubmonoid.closure s) (y : M) (hy : y ∈ AddSubmonoid.closure s),
p x hx → p y hy → p (x + y) ⋯) →
∀ {x : M} (hx : x ∈ AddSubmonoid.closure s), p x hx
This theorem, named `AddSubmonoid.closure_induction'`, is a dependent form of the `AddSubmonoid.closure_induction` theorem. It states that for any type `M` with an `AddZeroClass` instance, any set `s` of `M`, and any property `p` that can be assigned to each element of the closure of `s` under the add submonoid operation, if `p` holds for all elements in `s`, and `p` also holds for `0`, and if for any two elements `x` and `y` in the closure, if `p` holds for `x` and `y` then it also holds for `x + y`, then `p` must hold for all elements in the closure of `s`. The `⋯` in the statement represents additional conditions or details that have been omitted for brevity.
More concisely: If `s` is a set in an additive submonoid of a type `M` with an `AddZeroClass` instance, and `p` is a property that holds for all elements in `s` and is closed under addition, then `p` holds for all elements in the closure of `s`.
|
AddMonoidHom.eq_of_eqOn_denseM
theorem AddMonoidHom.eq_of_eqOn_denseM :
∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {s : Set M},
AddSubmonoid.closure s = ⊤ → ∀ {f g : M →+ N}, Set.EqOn (⇑f) (⇑g) s → f = g
The theorem `AddMonoidHom.eq_of_eqOn_denseM` states that for any types `M` and `N` which are instances of the `AddZeroClass`, and for any set `s` of type `M`, if the additive submonoid generated by `s` is the entire set (i.e., `AddSubmonoid.closure s = ⊤` where `⊤` denotes the total set), then for any two additive monoid homomorphisms `f` and `g` from `M` to `N`, if `f` and `g` are equal on the set `s` (i.e., `Set.EqOn (⇑f) (⇑g) s` where `⇑f` and `⇑g` are the application of the functions `f` and `g` respectively), then `f` and `g` are equal everywhere. In other words, in the context of additive monoid homomorphisms, knowing that two functions are equal on a densely populated set implies that they are equal everywhere.
More concisely: If `M` and `N` are AddZeroClasses, `s` is the dense additive submonoid of `M`, and `f` and `g` are additive monoid homomorphisms from `M` to `N` that agree on `s`, then `f = g`.
|
Submonoid.subset_closure
theorem Submonoid.subset_closure : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M}, s ⊆ ↑(Submonoid.closure s) := by
sorry
This theorem states that for any type `M` which has a multiplication and a one (i.e., it is an instance of `MulOneClass`), and any set `s` of elements in `M`, the set `s` is a subset of the submonoid generated by `s`. In other words, every element in the set `s` is also an element in the submonoid that is generated by `s`. The submonoid generated by `s` is the smallest submonoid that contains `s`, so this theorem essentially says all elements of `s` are also included in this smallest containing submonoid. This is expressed by the inclusion relation `s ⊆ ↑(Submonoid.closure s)`.
More concisely: For any multiplicative monoid `M` and subset `s` of `M`, `s` is contained in the submonoid generated by `s` (i.e., `s ⊆ Submonoid.closure s`).
|
Submonoid.closure_mono
theorem Submonoid.closure_mono :
∀ {M : Type u_1} [inst : MulOneClass M] ⦃s t : Set M⦄, s ⊆ t → Submonoid.closure s ≤ Submonoid.closure t
The theorem `Submonoid.closure_mono` states that for any type `M` equipped with an instance of `MulOneClass` (which means `M` is a monoid), the closure operation over submonoids is monotonic with respect to set inclusion. In other words, if we have two sets `s` and `t` of type `M` such that `s` is a subset of `t` (denoted as `s ⊆ t`), then the submonoid generated by `s` is a submonoid of (or equal to) the submonoid generated by `t` (denoted as `Submonoid.closure s ≤ Submonoid.closure t`). This theorem captures the intuitive idea that enlarging the generating set of a submonoid can only result in a larger submonoid.
More concisely: For any monoid `M` with instance of `MulOneClass`, the closure operation on submonoids is monotonic, that is, the submonoid generated by a subset is included in the submonoid generated by any superset.
|
AddSubmonoid.closure_induction₂
theorem AddSubmonoid.closure_induction₂ :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {p : M → M → Prop} {x y : M},
x ∈ AddSubmonoid.closure s →
y ∈ AddSubmonoid.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x : M), p 0 x) →
(∀ (x : M), p x 0) →
(∀ (x y z : M), p x z → p y z → p (x + y) z) → (∀ (x y z : M), p z x → p z y → p z (x + y)) → p x y
The theorem `AddSubmonoid.closure_induction₂` is an induction principle for additive closure membership for predicates with two arguments. Given a type `M` that is an additive group with zero (`AddZeroClass M`), a set `s` of elements of `M`, a predicate `p` on pairs of elements of `M`, and two arbitrary elements `x` and `y` of `M`. If `x` and `y` are in the additive submonoid generated by `s` (i.e., the smallest additive submonoid that includes `s`), and if the predicate `p` holds for all pairs of elements within `s`, for all elements paired with zero, for the addition of any two elements where the predicate holds, and for the addition of any two elements where the predicate holds with the arguments reversed, then the predicate `p` should hold for `x` and `y`.
More concisely: If `s` is an additive submonoid of an additive group `M`, `p` is a predicate on pairs of elements in `M` that satisfies `p(x, y)` whenever `x`, `y` are in `s` or `x = 0` or `y = 0`, and `x`, `y` are in the additive submonoid generated by `s`, then `p(x, y)` holds.
|
nsmul_mem
theorem nsmul_mem :
∀ {M : Type u_4} {A : Type u_5} [inst : AddMonoid M] [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M] {S : A}
{x : M}, x ∈ S → ∀ (n : ℕ), n • x ∈ S
This theorem states that for any two types `M` and `A`, where `M` is an additive monoid and `A` behaves like a set of elements of `M` (`SetLike A M`), and `A` has the properties of an additive submonoid of `M` (`AddSubmonoidClass A M`), then for any `S` of type `A` and any element `x` of type `M`, if `x` belongs to `S`, then the n-fold addition of `x` (denoted `n • x`) also belongs to `S` for any non-negative integer `n`. In simpler terms, it's saying that adding an element to itself any number of times in an additive submonoid results in a value that is also in that submonoid.
More concisely: For any additive submonoid `A` of an additive monoid `M`, if `x` is an element of `A` and `n` is a non-negative integer, then `n • x` is also an element of `A`.
|
Submonoid.closure_induction
theorem Submonoid.closure_induction :
∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {p : M → Prop} {x : M},
x ∈ Submonoid.closure s → (∀ x ∈ s, p x) → p 1 → (∀ (x y : M), p x → p y → p (x * y)) → p x
This theorem, called "Submonoid.closure_induction", is an induction principle for checking if an element is a member of a submonoid's closure. Given a type `M` with multiplication and identity (`MulOneClass M`), a set `s` of type `M`, a predicate `p` from `M` to `Prop`, and an element `x` of type `M`, it states that if `x` is in the closure of `s`, `p` holds for the multiplicative identity `1` and all elements of `s`, and `p` is preserved under multiplication (i.e., if `p` holds for elements `x` and `y`, then it also holds for their product `x * y`), then `p` holds for `x`. In other words, we can use this theorem to prove properties of elements in the generated submonoid by showing they hold for `1`, the generating set `s`, and are preserved under multiplication.
More concisely: If `s` is a submonoid of a type `M` with predicate `p`, and `x` is in the closure of `s` with `p(1)` holding for the multiplicative identity and `p` being multiplicatively preserving on `s`, then `p(x)` holds.
|
AddSubmonoid.zero_mem'
theorem AddSubmonoid.zero_mem' : ∀ {M : Type u_4} [inst : AddZeroClass M] (self : AddSubmonoid M), 0 ∈ self.carrier
This theorem, `AddSubmonoid.zero_mem'`, asserts that for any type `M` that is a member of the `AddZeroClass` class (i.e., it supports the operations of addition and has a zero element), the element `0` belongs to the carrier of any additive submonoid of `M`. In simpler terms, the zero of the type `M` is always an element of any of its additive submonoids.
More concisely: For any type `M` in the `AddZeroClass`, the zero element of `M` belongs to every additive submonoid of `M`.
|
AddSubmonoid.closure_union
theorem AddSubmonoid.closure_union :
∀ {M : Type u_1} [inst : AddZeroClass M] (s t : Set M),
AddSubmonoid.closure (s ∪ t) = AddSubmonoid.closure s ⊔ AddSubmonoid.closure t
This theorem, `AddSubmonoid.closure_union`, states that for any type `M` that has an addition and zero operation (captured by the `AddZeroClass` typeclass), and for any two sets `s` and `t` of this type `M`, the additive submonoid generated by the union of these two sets (`s ∪ t`) is equal to the supremum (the least upper bound or "join", denoted by `⊔`) of the additive submonoids generated by each of these sets separately (`s` and `t`). Essentially, it shows a distributive property of the closure operation over the union of sets in the context of additive submonoids.
More concisely: The additive submonoid generated by the union of two sets is equal to the supremum of the additive submonoids generated by each set.
|
Submonoid.closure_induction'
theorem Submonoid.closure_induction' :
∀ {M : Type u_1} [inst : MulOneClass M] (s : Set M) {p : (x : M) → x ∈ Submonoid.closure s → Prop},
(∀ (x : M) (h : x ∈ s), p x ⋯) →
p 1 ⋯ →
(∀ (x : M) (hx : x ∈ Submonoid.closure s) (y : M) (hy : y ∈ Submonoid.closure s),
p x hx → p y hy → p (x * y) ⋯) →
∀ {x : M} (hx : x ∈ Submonoid.closure s), p x hx
The theorem `Submonoid.closure_induction'` states that for any type `M` with a multiplication and a one (`MulOneClass M`), any set `s` of elements of `M`, and any property `p` that depends on an element of the closure of `s` (i.e., the smallest submonoid containing `s`), if the following conditions are met:
1. The property `p` holds for all elements in the set `s`.
2. The property `p` holds for the identity element `1`.
3. For any two elements `x` and `y` in the closure of `s`, if `p` holds for `x` and `y`, then `p` also holds for the product `x * y`.
Then the property `p` holds for all elements in the closure of `s`. This theorem is a dependent type version of the inductive principle for the closure of a set in a monoid.
More concisely: If `s` is a set of elements in a monoid `M` with multiplication and one, such that `p(x)` holds for all `x` in `s` and `p(x * y)` holds for all `x, y` in the closure of `s`, then `p` holds for all elements in the closure of `s`.
|
AddSubmonoid.subset_closure
theorem AddSubmonoid.subset_closure :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M}, s ⊆ ↑(AddSubmonoid.closure s)
The theorem `AddSubmonoid.subset_closure` states that for any type `M` that has an `AddZeroClass` instance (i.e., `M` is a type where addition and zero are defined), and for any set `s` of elements of type `M`, the set `s` is a subset of the `AddSubmonoid` generated by `s`. In other words, every element of the set `s` is included in the additive submonoid that is generated by `s`.
More concisely: For any AddZeroClass type M and set s of its elements, s is contained in the AddSubmonoid generated by s.
|
Mathlib.GroupTheory.Submonoid.Basic._auxLemma.10
theorem Mathlib.GroupTheory.Submonoid.Basic._auxLemma.10 :
∀ {M : Type u_1} [inst : MulOneClass M] (x : M), (x ∈ ⊤) = True
This theorem states that for any type `M` that has a multiplication operation and an identity element (i.e., `M` is a `MulOneClass`), any element `x` of type `M` is a member of the top submonoid (denoted as `⊤`). In other words, the top submonoid contains all elements of the `MulOneClass`.
More concisely: For any `MulOneClass` type `M` and its element `x`, `x` belongs to the top submonoid `⊤` of `M`.
|
Submonoid.dense_induction
theorem Submonoid.dense_induction :
∀ {M : Type u_1} [inst : MulOneClass M] {p : M → Prop} (x : M) {s : Set M},
Submonoid.closure s = ⊤ → (∀ x ∈ s, p x) → p 1 → (∀ (x y : M), p x → p y → p (x * y)) → p x
This theorem, called `Submonoid.dense_induction`, states that if we have a set `s` that is dense in a monoid `M` (i.e., the submonoid generated by `s` equals the total monoid, `Submonoid.closure s = ⊤`), we can prove a predicate `p` holds for all elements in `M` by just proving three things: `p` holds for all elements in `s`, `p` holds for the identity element `1` of the monoid, and `p` is preserved under the monoid operation, i.e., if `p` holds for elements `x` and `y`, then `p` also holds for their product `x * y`. If these conditions are met, the theorem assures us that `p` holds for any element `x` in the monoid `M`.
More concisely: If a subset `s` of a monoid `M` is dense (i.e., generates the entire monoid), then any predicate `p` holding for all elements in `s` and the identity `1` and preserving the monoid operation `*` also holds for every element in `M`.
|
Mathlib.GroupTheory.Submonoid.Basic._auxLemma.8
theorem Mathlib.GroupTheory.Submonoid.Basic._auxLemma.8 :
∀ {M : Type u_1} [inst : MulOneClass M] {x : M}, (x ∈ ⊥) = (x = 1)
This theorem states that for any type `M` which has a structure of `MulOneClass` (meaning it has multiplication and a multiplicative identity), a given element `x` of type `M` belongs to the trivial subgroup (denoted by `⊥`) if and only if `x` is equal to the multiplicative identity (denoted by `1`). In mathematical terms, for any element `x` in a multiplication-inclusive set with identity, `x` is in the trivial group if and only if `x` equals the identity.
More concisely: For any type `M` with multiplication and identity, an element `x` in `M` lies in the trivial subgroup if and only if `x = 1`.
|
Submonoid.mul_mem
theorem Submonoid.mul_mem :
∀ {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) {x y : M}, x ∈ S → y ∈ S → x * y ∈ S
This theorem states that a submonoid is closed under multiplication. In the context of any type `M` equipped with multiplication and a neutral element ("one"), if `S` is a submonoid of `M`, and if `x` and `y` are elements of `S`, then the multiplication of `x` and `y` (denoted `x * y`) is also an element of `S`. This is a fundamental property of submonoids: they are subsets of monoids that are also monoids with the inherited operation.
More concisely: If `S` is a submonoid of a monoid `M` with multiplication `*` and neutral element `one`, then `x * y` belongs to `S` for all `x, y` in `S`.
|
Mathlib.GroupTheory.Submonoid.Basic._auxLemma.11
theorem Mathlib.GroupTheory.Submonoid.Basic._auxLemma.11 :
∀ {M : Type u_1} [inst : AddZeroClass M] (x : M), (x ∈ ⊤) = True
This theorem, named `Mathlib.GroupTheory.Submonoid.Basic._auxLemma.11`, asserts that for any type `M` that has an addition operation and a zero element (i.e., `M` is an instance of the `AddZeroClass`), any element `x` of type `M` always belongs to the top element of the lattice structure (`⊤`). In other words, it states that every element of an additive monoid with a zero element is contained in the largest (top) submonoid.
More concisely: For any additive monoid `M` with a zero element, every `x` in `M` belongs to the top element (lattice unit) of `M`.
|
OneMemClass.one_mem
theorem OneMemClass.one_mem :
∀ {S : Type u_4} {M : Type u_5} [inst : One M] [inst_1 : SetLike S M] [self : OneMemClass S M] (s : S), 1 ∈ s := by
sorry
This theorem states that if we have an instance of `OneMemClass S M`, then the number 1 is an element of any set `s` of type `S`. Here, `S` is a type that behaves like a set of elements of type `M`, and `M` is a type that has a defined concept of `One`. Hence, the theorem asserts that for all `s : S`, we have `1 ∈ s`.
More concisely: If `S` is a type of sets with elements of type `M`, and `M` has a defined concept of `One`, then for every `s : S`, the element `1` belongs to `s`.
|
AddSubmonoid.mem_bot
theorem AddSubmonoid.mem_bot : ∀ {M : Type u_1} [inst : AddZeroClass M] {x : M}, x ∈ ⊥ ↔ x = 0
This theorem states that for any type `M` that belongs to the `AddZeroClass` class (meaning that it has a zero element and an addition operation), an element `x` of type `M` belongs to the bottom AddSubmonoid (which contains only the zero element) if and only if `x` is equal to zero. In mathematical terms, this theorem is saying that the only element in the trivial additive submonoid is the zero element.
More concisely: For any type `M` in the `AddZeroClass`, an element `x` of `M` belongs to the bottom AddSubmonoid if and only if `x = 0`.
|
AddSubmonoid.mem_closure
theorem AddSubmonoid.mem_closure :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {x : M},
x ∈ AddSubmonoid.closure s ↔ ∀ (S : AddSubmonoid M), s ⊆ ↑S → x ∈ S
This theorem states that for any type `M` that is an instance of `AddZeroClass` (which means `M` is a set with addition and zero), any set `s` of elements of `M`, and any element `x` of `M`, `x` is an element of the additive submonoid generated by `s` if and only if for all additive submonoids `S` of `M` such that `s` is a subset of `S`, `x` is also an element of `S`. This is essentially describing the closure property of a submonoid: an element is in the closure of a set if it is in every submonoid that contains the set.
More concisely: For any set `s` of elements from an additive semigroup `M` with zero `0`, an element `x` belongs to the additive submonoid generated by `s` if and only if `x` is in every submonoid containing `s`.
|
Submonoid.mem_top
theorem Submonoid.mem_top : ∀ {M : Type u_1} [inst : MulOneClass M] (x : M), x ∈ ⊤
This theorem states that for any given type `M` (which is a multiplication class with a multiplicative identity), every element `x` of type `M` belongs to the top submonoid `⊤`. In the context of abstract algebra, a submonoid is a subset of a monoid that is closed under the monoid operation and contains the identity element of the monoid. The top submonoid `⊤` is the whole monoid itself, hence every element of the monoid belongs to it.
More concisely: Every element of a multiplication class `M` with an identity belongs to the top submonoid `⊤` (equivalent to the monoid itself).
|
AddSubmonoid.ext
theorem AddSubmonoid.ext :
∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M}, (∀ (x : M), x ∈ S ↔ x ∈ T) → S = T
This theorem states that two addition submonoids (`AddSubmonoid`s) `S` and `T` of a certain type `M` (which forms an additive zero class) are equal if they contain exactly the same elements. Formally, if for every element `x` of type `M`, `x` belongs to `S` if and only if `x` belongs to `T`, then `S` and `T` must be equal.
More concisely: If two additive submonoids `S` and `T` of an additive zero class `M` in Lean 4 have the same elements, then `S` is equal to `T`.
|
Submonoid.closure_union
theorem Submonoid.closure_union :
∀ {M : Type u_1} [inst : MulOneClass M] (s t : Set M),
Submonoid.closure (s ∪ t) = Submonoid.closure s ⊔ Submonoid.closure t
This theorem states that for any type `M` that has a multiplication and a multiplicative identity (captured by the `MulOneClass M` typeclass in Lean), and for any two sets `s` and `t` of this type `M`, the submonoid generated by the union of `s` and `t` is equal to the join (supremum) of the submonoids generated by `s` and `t` respectively. In other words, the submonoid generated by the union of two sets is the smallest submonoid that contains both the submonoid generated by each individual set.
More concisely: For any type `M` with multiplication and multiplicative identity, the submonoid generated by the union of two sets `s` and `t` in `M` equals the join (supremum) of the submonoids generated by `s` and `t`.
|
AddSubmonoid.add_mem
theorem AddSubmonoid.add_mem :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) {x y : M}, x ∈ S → y ∈ S → x + y ∈ S
This theorem states that an `AddSubmonoid` is closed under the operation of addition. In more detail, given a type `M` which is an instance of the `AddZeroClass` (that is, it supports addition operation and has a zero), if `S` is an `AddSubmonoid` of `M`, then for any two elements `x` and `y` in `M`, if both `x` and `y` belong to `S`, then their sum `x + y` also belongs to `S`. In other words, adding two elements of the submonoid results in another element of the same submonoid, thus ensuring closure under addition.
More concisely: If `S` is an additive submonoid of an additive semigroup with zero, then for all `x, y ∈ S`, `x + y ∈ S`.
|
AddSubmonoid.dense_induction
theorem AddSubmonoid.dense_induction :
∀ {M : Type u_1} [inst : AddZeroClass M] {p : M → Prop} (x : M) {s : Set M},
AddSubmonoid.closure s = ⊤ → (∀ x ∈ s, p x) → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → p x
The theorem `AddSubmonoid.dense_induction` states that for a given type `M` with `AddZeroClass` structure, a predicate `p` on `M`, an element `x` of `M`, and a subset `s` of `M` that densely generates `M` as an additive submonoid (i.e., the closure of `s` equals the entire set of `M`), if the following three conditions are met:
1) the predicate `p` holds for all elements in `s`,
2) the predicate `p` holds for the zero element, and
3) for any two elements `x` and `y` in `M`, if `p` holds for both `x` and `y`, then `p` also holds for the sum `x + y`,
then we can conclude that the predicate `p` holds for all elements in `M`. In other words, it gives a method of proving that a property holds for all elements in an additive monoid, given that the property holds for a dense subset and is preserved under addition and zero.
More concisely: If a predicate holds for all elements in a densely generating subset of an additive submonoid and is closed under addition and zero, then it holds for all elements in the submonoid.
|
AddSubmonoid.closure_le
theorem AddSubmonoid.closure_le :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M}, AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S := by
sorry
The theorem `AddSubmonoid.closure_le` states that for any type `M` equipped with an additive zero class structure, any set `s` of elements of type `M`, and any additive submonoid `S` of type `M`, the additive submonoid generated by `s` (denoted `AddSubmonoid.closure s`) is contained within `S` if and only if the set `s` is a subset of the underlying set of `S`, denoted as `↑S`. In other words, the theorem provides a criterion for an additive submonoid to contain the submonoid generated by a certain set.
More concisely: For any additive zero class structure on a type `M`, a set `s` of `M` is contained in the additive submonoid generated by `s` if and only if `s` is a subset of an additive submonoid `S` of `M`.
|
Submonoid.coe_iInf
theorem Submonoid.coe_iInf :
∀ {M : Type u_1} [inst : MulOneClass M] {ι : Sort u_4} {S : ι → Submonoid M}, ↑(⨅ i, S i) = ⋂ i, ↑(S i)
This theorem states that for any type `M` with a multiplication and identity operation (captured by `MulOneClass M`), and for any indexing type `ι` with given submonoids `S : ι → Submonoid M`, the coercion of the infimum (greatest lower bound) of the `S i` for all `i` (represented by `⨅ i, S i`) is equal to the intersection over all `i` of the coercion of `S i` (represented by `⋂ i, ↑(S i)`). In simpler terms, the intersection of a collection of submonoids is itself a submonoid.
More concisely: For any type `M` with multiplication and identity, and for any indexing type `ι` with submonoids `S i`, the infimum of `S i` for all `i` equals the intersection of the coercions of `S i`. (In other words, the intersection of submonoids is itself a submonoid.)
|
AddSubmonoid.closure_eq
theorem AddSubmonoid.closure_eq :
∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), AddSubmonoid.closure ↑S = S
This theorem states that, for any additive submonoid `S` of a type `M` equipped with an addition operation and a zero element (represented by the `AddZeroClass M` instance), the additive closure of `S` equals `S` itself. In other words, if we take an additive submonoid and generate the smallest additive submonoid that contains it (the "additive closure of `S`"), we end up with the original submonoid `S`. This implies that `S` already contains all elements that can be obtained through repeated addition operations on its elements.
More concisely: The additive closure of an additive submonoid equals the submonoid itself.
|
ZeroMemClass.zero_mem
theorem ZeroMemClass.zero_mem :
∀ {S : Type u_4} {M : Type u_5} [inst : Zero M] [inst_1 : SetLike S M] [self : ZeroMemClass S M] (s : S), 0 ∈ s
This theorem states that for any types `S` and `M`, given that `M` has a zero element and `S` has a `SetLike` structure (meaning that `S` behaves like a set of elements from `M`), if `S` and `M` form a `ZeroMemClass` (a structure implying that the zero element of `M` is contained in every element of `S`), then the zero element of `M` is indeed a member of any given element of `S`. In other words, if `s` is an element of type `S`, then `0` belongs to `s`.
More concisely: If `S` is a `SetLike` type over `M` that is a `ZeroMemClass`, then the zero element of `M` is an element of every element `s` in `S`.
|
AddSubmonoid.closure_mono
theorem AddSubmonoid.closure_mono :
∀ {M : Type u_1} [inst : AddZeroClass M] ⦃s t : Set M⦄, s ⊆ t → AddSubmonoid.closure s ≤ AddSubmonoid.closure t
The theorem `AddSubmonoid.closure_mono` states that for any type `M` that has an addition and zero structure (expressed by `[AddZeroClass M]`), the closure operation of an additive submonoid is monotone with respect to the set containment order. In other words, if you have two sets `s` and `t` of elements of type `M` and `s` is a subset of `t` (expressed by `s ⊆ t`), then the additive submonoid generated by `s` (expressed by `AddSubmonoid.closure s`) is a submonoid of (or equal to) the additive submonoid generated by `t` (expressed by `AddSubmonoid.closure t`).
More concisely: For any type `M` with an addition and zero structure, the closure of an additive submonoid under a subset inclusion relation is inclusion preserving.
|
AddSubmonoid.closure_induction
theorem AddSubmonoid.closure_induction :
∀ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {p : M → Prop} {x : M},
x ∈ AddSubmonoid.closure s → (∀ x ∈ s, p x) → p 0 → (∀ (x y : M), p x → p y → p (x + y)) → p x
The theorem `AddSubmonoid.closure_induction` is an induction principle for membership in the additive closure of a set. In more detail, for any type `M` that is an instance of `AddZeroClass`, a set `s` of elements of type `M`, and a property `p` that holds for each element of type `M`, if an element `x` belongs to the additive closure of the set `s`, `p` holds for `0` and all elements of `s`, and `p` is preserved under addition, then `p` also holds for `x`. In other words, any property of elements of the original set that is closed under addition and holds for the additive identity, also holds for all elements in the additive closure of the set.
More concisely: If `s` is a set of additive elements in an additive semigroup `M` such that for all `x` in the additive closure of `s`, `p(x)` holds whenever `p(0)` holds and `p(x)` is the sum of `p(a)` and `p(b)` for any `a, b` in `s`, then `p` holds for all elements in the additive closure of `s`.
|
pow_mem
theorem pow_mem :
∀ {M : Type u_4} {A : Type u_5} [inst : Monoid M] [inst_1 : SetLike A M] [inst_2 : SubmonoidClass A M] {S : A}
{x : M}, x ∈ S → ∀ (n : ℕ), x ^ n ∈ S
This theorem states that for any given type `M` with a Monoid structure and another type `A` that behaves like a set of `M` (with `S` as an instance of `A`), if an element `x` of type `M` belongs to `S`, then `x` raised to the power of any natural number `n` also belongs to `S`. In other words, if `x` is an element of a given submonoid `S`, then all powers of `x` are also elements of `S`.
More concisely: If `x` is an element of a submonoid `S` of a monoid `M`, then for all natural numbers `n`, `x^n` is also an element of `S`.
|
Submonoid.closure_induction₂
theorem Submonoid.closure_induction₂ :
∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {p : M → M → Prop} {x y : M},
x ∈ Submonoid.closure s →
y ∈ Submonoid.closure s →
(∀ x ∈ s, ∀ y ∈ s, p x y) →
(∀ (x : M), p 1 x) →
(∀ (x : M), p x 1) →
(∀ (x y z : M), p x z → p y z → p (x * y) z) → (∀ (x y z : M), p z x → p z y → p z (x * y)) → p x y
This theorem is an induction principle for the membership in the closure of a submonoid, when dealing with predicates that take two arguments. For any type `M` with `MulOneClass` instance, a set `s` of `M`, a predicate `p` mapping two elements of `M`, and elements `x` and `y` of `M`, the theorem states that if `x` and `y` are in the closure of the submonoid generated by `s`, and given that the predicate `p` holds for any two elements in `s`, and for any element `x` of `M`, `p` holds for `1` and `x` and `x` and `1`, and if `p` holds for `x` and `z`, and `y` and `z`, then `p` also holds for the product of `x` and `y` and `z`, and also if `p` holds for `z` and `x`, `z` and `y`, then `p` also holds for `z` and the product of `x` and `y`, then `p` holds for `x` and `y`. In simpler terms, it allows us to establish properties of two elements in the submonoid produced by the closure, assuming certain properties of the set elements and their multiplications.
More concisely: If `s` is a submonoid of a `MulOneClass` type `M`, `p` is a binary predicate satisfying certain conditions on `s` and `M`, and `x`, `y`, and `z` are in the closure of `s`, then `p(x, y)` holds if and only if `p(1, x)`, `p(x, 1)`, `p(x, z)`, `p(y, z)`, `p(z, x)`, and `p(z, y)` hold.
|