Documentation

Mathlib.Deprecated.Submonoid

Unbundled submonoids (deprecated) #

This file is deprecated, and is no longer imported by anything in mathlib other than other deprecated files, and test files. You should not need to import it.

This file defines unbundled multiplicative and additive submonoids. Instead of using this file, please use Submonoid G and AddSubmonoid A, defined in GroupTheory.Submonoid.Basic.

Main definitions #

IsAddSubmonoid (S : Set M) : the predicate that S is the underlying subset of an additive submonoid of M. The bundled variant AddSubmonoid M should be used in preference to this.

IsSubmonoid (S : Set M) : the predicate that S is the underlying subset of a submonoid of M. The bundled variant Submonoid M should be used in preference to this.

Tags #

Submonoid, Submonoids, IsSubmonoid

structure IsAddSubmonoid {A : Type u_1} [inst : AddMonoid A] (s : Set A) :

The proposition that s contains 0.
zero_mem : 0 ∈ s
The proposition that s is closed under addition.
add_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a + b ∈ s

s is an additive submonoid: a set containing 0 and closed under addition. Note that this structure is deprecated, and the bundled variant AddSubmonoid A should be preferred.

Instances For

structure IsSubmonoid {M : Type u_1} [inst : Monoid M] (s : Set M) :

The proposition that s contains 1.
one_mem : 1 ∈ s
The proposition that s is closed under multiplication.
mul_mem : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s

s is a submonoid: a set containing 1 and closed under multiplication. Note that this structure is deprecated, and the bundled variant Submonoid M should be preferred.

Instances For

theorem Additive.isAddSubmonoid {M : Type u_1} [inst : Monoid M] {s : Set M} :

IsSubmonoid s → IsAddSubmonoid s

theorem Additive.isAddSubmonoid_iff {M : Type u_1} [inst : Monoid M] {s : Set M} :

IsAddSubmonoid s ↔ IsSubmonoid s

theorem Multiplicative.isSubmonoid {A : Type u_1} [inst : AddMonoid A] {s : Set A} :

IsAddSubmonoid s → IsSubmonoid s

theorem Multiplicative.isSubmonoid_iff {A : Type u_1} [inst : AddMonoid A] {s : Set A} :

IsSubmonoid s ↔ IsAddSubmonoid s

theorem IsAddSubmonoid.inter {M : Type u_1} [inst : AddMonoid M] {s₁ : Set M} {s₂ : Set M} (is₁ : IsAddSubmonoid s₁) (is₂ : IsAddSubmonoid s₂) :

IsAddSubmonoid (s₁ ∩ s₂)

The intersection of two AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

theorem IsSubmonoid.inter {M : Type u_1} [inst : Monoid M] {s₁ : Set M} {s₂ : Set M} (is₁ : IsSubmonoid s₁) (is₂ : IsSubmonoid s₂) :

IsSubmonoid (s₁ ∩ s₂)

The intersection of two submonoids of a monoid M is a submonoid of M.

theorem IsAddSubmonoid.interᵢ {M : Type u_2} [inst : AddMonoid M] {ι : Sort u_1} {s : ι → Set M} (h : ∀ (y : ι), IsAddSubmonoid (s y)) :

IsAddSubmonoid (Set.interᵢ s)

The intersection of an indexed set of AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

theorem IsSubmonoid.interᵢ {M : Type u_2} [inst : Monoid M] {ι : Sort u_1} {s : ι → Set M} (h : ∀ (y : ι), IsSubmonoid (s y)) :

IsSubmonoid (Set.interᵢ s)

The intersection of an indexed set of submonoids of a monoid M is a submonoid of M.

abbrev isAddSubmonoid_unionᵢ_of_directed.match_3 {M : Type u_2} {ι : Type u_1} {s : ι → Set M} :

{b : M} → (motive : (∃ i, b ∈ s i) → Prop) → ∀ (x : ∃ i, b ∈ s i), (∀ (j : ι) (hj : b ∈ s j), motive (_ : ∃ i, b ∈ s i)) → motive x

Equations

isAddSubmonoid_unionᵢ_of_directed.match_3 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

abbrev isAddSubmonoid_unionᵢ_of_directed.match_2 {M : Type u_2} {ι : Type u_1} {s : ι → Set M} (i : ι) (j : ι) (motive : (∃ k, s i ⊆ s k ∧ s j ⊆ s k) → Prop) :

(x : ∃ k, s i ⊆ s k ∧ s j ⊆ s k) → ((k : ι) → (hk : s i ⊆ s k ∧ s j ⊆ s k) → motive (_ : ∃ k, s i ⊆ s k ∧ s j ⊆ s k)) → motive x

Equations

isAddSubmonoid_unionᵢ_of_directed.match_2 i j motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem isAddSubmonoid_unionᵢ_of_directed {M : Type u_2} [inst : AddMonoid M] {ι : Type u_1} [hι : Nonempty ι] {s : ι → Set M} (hs : ∀ (i : ι), IsAddSubmonoid (s i)) (Directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k) :

IsAddSubmonoid (Set.unionᵢ fun i => s i)

The union of an indexed, directed, nonempty set of AddSubmonoids of an AddMonoid M is an AddSubmonoid of M.

abbrev isAddSubmonoid_unionᵢ_of_directed.match_1 {ι : Type u_1} (motive : Nonempty ι → Prop) :

(hι : Nonempty ι) → ((i : ι) → motive (_ : Nonempty ι)) → motive hι

Equations

isAddSubmonoid_unionᵢ_of_directed.match_1 motive hι h_1 = Nonempty.casesOn hι fun val => h_1 val

theorem isSubmonoid_unionᵢ_of_directed {M : Type u_2} [inst : Monoid M] {ι : Type u_1} [hι : Nonempty ι] {s : ι → Set M} (hs : ∀ (i : ι), IsSubmonoid (s i)) (Directed : ∀ (i j : ι), ∃ k, s i ⊆ s k ∧ s j ⊆ s k) :

IsSubmonoid (Set.unionᵢ fun i => s i)

The union of an indexed, directed, nonempty set of submonoids of a monoid M is a submonoid of M.

def multiples {M : Type u_1} [inst : AddMonoid M] (x : M) :

The set of natural number multiples 0, x, 2x, ... of an element x of an AddMonoid.

Equations

multiples x = { y | ∃ n, n • x = y }

def powers {M : Type u_1} [inst : Monoid M] (x : M) :

The set of natural number powers 1, x, x², ... of an element x of a monoid.

Equations

powers x = { y | ∃ n, x ^ n = y }

theorem multiples.zero_mem {M : Type u_1} [inst : AddMonoid M] {x : M} :

0 ∈ multiples x

0 is in the set of natural number multiples of an element of an AddMonoid.

theorem powers.one_mem {M : Type u_1} [inst : Monoid M] {x : M} :

1 is in the set of natural number powers of an element of a monoid.

theorem multiples.self_mem {M : Type u_1} [inst : AddMonoid M] {x : M} :

x ∈ multiples x

An element of an AddMonoid is in the set of that element's natural number multiples.

theorem powers.self_mem {M : Type u_1} [inst : Monoid M] {x : M} :

An element of a monoid is in the set of that element's natural number powers.

abbrev multiples.add_mem.match_1 {M : Type u_1} [inst : AddMonoid M] {x : M} {z : M} (motive : z ∈ multiples x → Prop) :

(x : z ∈ multiples x) → ((n₂ : ℕ) → (h₂ : n₂ • x = z) → motive (_ : ∃ n, n • x = z)) → motive x

Equations

multiples.add_mem.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem multiples.add_mem {M : Type u_1} [inst : AddMonoid M] {x : M} {y : M} {z : M} :

y ∈ multiples x → z ∈ multiples x → y + z ∈ multiples x

The set of natural number multiples of an element of an AddMonoid is closed under addition.

theorem powers.mul_mem {M : Type u_1} [inst : Monoid M] {x : M} {y : M} {z : M} :

y ∈ powers x → z ∈ powers x → y * z ∈ powers x

The set of natural number powers of an element of a monoid is closed under multiplication.

theorem multiples.isAddSubmonoid {M : Type u_1} [inst : AddMonoid M] (x : M) :

IsAddSubmonoid (multiples x)

The set of natural number multiples of an element of an AddMonoid M is an AddSubmonoid of M.

theorem powers.isSubmonoid {M : Type u_1} [inst : Monoid M] (x : M) :

IsSubmonoid (powers x)

The set of natural number powers of an element of a monoid M is a submonoid of M.

theorem Univ.isAddSubmonoid {M : Type u_1} [inst : AddMonoid M] :

IsAddSubmonoid Set.univ

An AddMonoid is an AddSubmonoid of itself.

theorem Univ.isSubmonoid {M : Type u_1} [inst : Monoid M] :

IsSubmonoid Set.univ

A monoid is a submonoid of itself.

theorem IsAddSubmonoid.preimage {M : Type u_2} [inst : AddMonoid M] {N : Type u_1} [inst : AddMonoid N] {f : M → N} (hf : IsAddMonoidHom f) {s : Set N} (hs : IsAddSubmonoid s) :

IsAddSubmonoid (f ⁻¹' s)

The preimage of an AddSubmonoid under an AddMonoid hom is an AddSubmonoid of the domain.

theorem IsSubmonoid.preimage {M : Type u_2} [inst : Monoid M] {N : Type u_1} [inst : Monoid N] {f : M → N} (hf : IsMonoidHom f) {s : Set N} (hs : IsSubmonoid s) :

IsSubmonoid (f ⁻¹' s)

The preimage of a submonoid under a monoid hom is a submonoid of the domain.

theorem IsAddSubmonoid.image {M : Type u_2} [inst : AddMonoid M] {γ : Type u_1} [inst : AddMonoid γ] {f : M → γ} (hf : IsAddMonoidHom f) {s : Set M} (hs : IsAddSubmonoid s) :

IsAddSubmonoid (f '' s)

The image of an AddSubmonoid under an AddMonoid hom is an AddSubmonoid of the codomain.

abbrev IsAddSubmonoid.image.match_1 {M : Type u_2} {γ : Type u_1} {f : M → γ} {s : Set M} (b : γ) (motive : b ∈ f '' s → Prop) :

(x : b ∈ f '' s) → ((y : M) → (hy : y ∈ s ∧ f y = b) → motive (_ : ∃ a, a ∈ s ∧ f a = b)) → motive x

Equations

IsAddSubmonoid.image.match_1 b motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem IsSubmonoid.image {M : Type u_2} [inst : Monoid M] {γ : Type u_1} [inst : Monoid γ] {f : M → γ} (hf : IsMonoidHom f) {s : Set M} (hs : IsSubmonoid s) :

IsSubmonoid (f '' s)

The image of a submonoid under a monoid hom is a submonoid of the codomain.

theorem Range.isAddSubmonoid {M : Type u_2} [inst : AddMonoid M] {γ : Type u_1} [inst : AddMonoid γ] {f : M → γ} (hf : IsAddMonoidHom f) :

IsAddSubmonoid (Set.range f)

The image of an AddMonoid hom is an AddSubmonoid of the codomain.

theorem Range.isSubmonoid {M : Type u_2} [inst : Monoid M] {γ : Type u_1} [inst : Monoid γ] {f : M → γ} (hf : IsMonoidHom f) :

IsSubmonoid (Set.range f)

The image of a monoid hom is a submonoid of the codomain.

abbrev IsAddSubmonoid.nsmul_mem.match_1 (motive : ℕ → Prop) :

(x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive (Nat.succ n)) → motive x

Equations

IsAddSubmonoid.nsmul_mem.match_1 motive x h_1 h_2 = Nat.casesOn x (h_1 ()) fun n => h_2 n

theorem IsAddSubmonoid.nsmul_mem {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M} (hs : IsAddSubmonoid s) (h : a ∈ s) {n : ℕ} :

n • a ∈ s

An AddSubmonoid is closed under multiplication by naturals.

theorem IsSubmonoid.pow_mem {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M} (hs : IsSubmonoid s) (h : a ∈ s) {n : ℕ} :

a ^ n ∈ s

Submonoids are closed under natural powers.

theorem IsAddSubmonoid.multiples_subset {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M} (hs : IsAddSubmonoid s) (h : a ∈ s) :

multiples a ⊆ s

The set of natural number multiples of an element of an AddSubmonoid is a subset of the AddSubmonoid.

theorem IsSubmonoid.power_subset {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M} (hs : IsSubmonoid s) (h : a ∈ s) :

The set of natural number powers of an element of a submonoid is a subset of the submonoid.

theorem IsAddSubmonoid.list_sum_mem {M : Type u_1} [inst : AddMonoid M] {s : Set M} (hs : IsAddSubmonoid s) {l : List M} :

(∀ (x : M), x ∈ l → x ∈ s) → List.sum l ∈ s

The sum of a list of elements of an AddSubmonoid is an element of the AddSubmonoid.

abbrev IsAddSubmonoid.list_sum_mem.match_1 {M : Type u_1} {s : Set M} (motive : (x : List M) → (∀ (x_1 : M), x_1 ∈ x → x_1 ∈ s) → Prop) :

(x : List M) → (x_1 : ∀ (x_1 : M), x_1 ∈ x → x_1 ∈ s) → ((x : ∀ (x : M), x ∈ [] → x ∈ s) → motive [] x) → ((a : M) → (l : List M) → (h : ∀ (x : M), x ∈ a :: l → x ∈ s) → motive (a :: l) h) → motive x x_1

Equations

One or more equations did not get rendered due to their size.

theorem IsSubmonoid.list_prod_mem {M : Type u_1} [inst : Monoid M] {s : Set M} (hs : IsSubmonoid s) {l : List M} :

(∀ (x : M), x ∈ l → x ∈ s) → List.prod l ∈ s

The product of a list of elements of a submonoid is an element of the submonoid.

theorem IsAddSubmonoid.multiset_sum_mem {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} (hs : IsAddSubmonoid s) (m : Multiset M) :

(∀ (a : M), a ∈ m → a ∈ s) → Multiset.sum m ∈ s

The sum of a multiset of elements of an AddSubmonoid of an AddCommMonoid is an element of the AddSubmonoid.

theorem IsSubmonoid.multiset_prod_mem {M : Type u_1} [inst : CommMonoid M] {s : Set M} (hs : IsSubmonoid s) (m : Multiset M) :

(∀ (a : M), a ∈ m → a ∈ s) → Multiset.prod m ∈ s

The product of a multiset of elements of a submonoid of a CommMonoid is an element of the submonoid.

theorem IsAddSubmonoid.finset_sum_mem {M : Type u_1} {A : Type u_2} [inst : AddCommMonoid M] {s : Set M} (hs : IsAddSubmonoid s) (f : A → M) (t : Finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → (Finset.sum t fun b => f b) ∈ s

The sum of elements of an AddSubmonoid of an AddCommMonoid indexed by a Finset is an element of the AddSubmonoid.

abbrev IsAddSubmonoid.finset_sum_mem.match_1 {M : Type u_2} {A : Type u_1} {s : Set M} (f : A → M) (motive : (x : Finset A) → (∀ (b : A), b ∈ x → f b ∈ s) → Prop) :

(x : Finset A) → (x_1 : ∀ (b : A), b ∈ x → f b ∈ s) → ((m : Multiset A) → (hm : Multiset.Nodup m) → (x : ∀ (b : A), b ∈ { val := m, nodup := hm } → f b ∈ s) → motive { val := m, nodup := hm } x) → motive x x_1

Equations

IsAddSubmonoid.finset_sum_mem.match_1 f motive x x h_1 = Finset.casesOn A (fun x => (x_1 : ∀ (b : A), b ∈ x → f b ∈ s) → motive x x_1) x (fun val nodup x => h_1 val nodup x) x

theorem IsSubmonoid.finset_prod_mem {M : Type u_1} {A : Type u_2} [inst : CommMonoid M] {s : Set M} (hs : IsSubmonoid s) (f : A → M) (t : Finset A) :

(∀ (b : A), b ∈ t → f b ∈ s) → (Finset.prod t fun b => f b) ∈ s

The product of elements of a submonoid of a CommMonoid indexed by a Finset is an element of the submonoid.

inductive AddMonoid.InClosure {A : Type u_1} [inst : AddMonoid A] (s : Set A) :

A → Prop

basic: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A} {a : A}, a ∈ s → AddMonoid.InClosure s a
zero: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A}, AddMonoid.InClosure s 0
add: ∀ {A : Type u_1} [inst : AddMonoid A] {s : Set A} {a b : A}, AddMonoid.InClosure s a → AddMonoid.InClosure s b → AddMonoid.InClosure s (a + b)

The inductively defined membership predicate for the submonoid generated by a subset of a monoid.

Instances For

inductive Monoid.InClosure {M : Type u_1} [inst : Monoid M] (s : Set M) :

M → Prop

basic: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M}, a ∈ s → Monoid.InClosure s a
one: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M}, Monoid.InClosure s 1
mul: ∀ {M : Type u_1} [inst : Monoid M] {s : Set M} {a b : M}, Monoid.InClosure s a → Monoid.InClosure s b → Monoid.InClosure s (a * b)

The inductively defined membership predicate for the Submonoid generated by a subset of an monoid.

Instances For

def AddMonoid.Closure {M : Type u_1} [inst : AddMonoid M] (s : Set M) :

The inductively defined AddSubmonoid genrated by a subset of an AddMonoid.

Equations

AddMonoid.Closure s = { a | AddMonoid.InClosure s a }

def Monoid.Closure {M : Type u_1} [inst : Monoid M] (s : Set M) :

The inductively defined submonoid generated by a subset of a monoid.

Equations

Monoid.Closure s = { a | Monoid.InClosure s a }

theorem AddMonoid.closure.isAddSubmonoid {M : Type u_1} [inst : AddMonoid M] (s : Set M) :

IsAddSubmonoid (AddMonoid.Closure s)

theorem Monoid.closure.isSubmonoid {M : Type u_1} [inst : Monoid M] (s : Set M) :

IsSubmonoid (Monoid.Closure s)

theorem AddMonoid.subset_closure {M : Type u_1} [inst : AddMonoid M] {s : Set M} :

s ⊆ AddMonoid.Closure s

A subset of an AddMonoid is contained in the AddSubmonoid it generates.

theorem Monoid.subset_closure {M : Type u_1} [inst : Monoid M] {s : Set M} :

s ⊆ Monoid.Closure s

A subset of a monoid is contained in the submonoid it generates.

theorem AddMonoid.closure_subset {M : Type u_1} [inst : AddMonoid M] {s : Set M} {t : Set M} (ht : IsAddSubmonoid t) (h : s ⊆ t) :

AddMonoid.Closure s ⊆ t

The AddSubmonoid generated by a set is contained in any AddSubmonoid that contains the set.

theorem Monoid.closure_subset {M : Type u_1} [inst : Monoid M] {s : Set M} {t : Set M} (ht : IsSubmonoid t) (h : s ⊆ t) :

Monoid.Closure s ⊆ t

The submonoid generated by a set is contained in any submonoid that contains the set.

theorem AddMonoid.closure_mono {M : Type u_1} [inst : AddMonoid M] {s : Set M} {t : Set M} (h : s ⊆ t) :

AddMonoid.Closure s ⊆ AddMonoid.Closure t

Given subsets t and s of an AddMonoid M, if s ⊆ t⊆ t, the AddSubmonoid of M generated by s is contained in the AddSubmonoid generated by t.

theorem Monoid.closure_mono {M : Type u_1} [inst : Monoid M] {s : Set M} {t : Set M} (h : s ⊆ t) :

Monoid.Closure s ⊆ Monoid.Closure t

Given subsets t and s of a monoid M, if s ⊆ t⊆ t, the submonoid of M generated by s is contained in the submonoid generated by t.

theorem AddMonoid.closure_singleton {M : Type u_1} [inst : AddMonoid M] {x : M} :

AddMonoid.Closure {x} = multiples x

The AddSubmonoid generated by an element of an AddMonoid equals the set of natural number multiples of the element.

theorem Monoid.closure_singleton {M : Type u_1} [inst : Monoid M] {x : M} :

Monoid.Closure {x} = powers x

The submonoid generated by an element of a monoid equals the set of natural number powers of the element.

theorem AddMonoid.image_closure {M : Type u_2} [inst : AddMonoid M] {A : Type u_1} [inst : AddMonoid A] {f : M → A} (hf : IsAddMonoidHom f) (s : Set M) :

f '' AddMonoid.Closure s = AddMonoid.Closure (f '' s)

The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set under the AddMonoid hom.

theorem Monoid.image_closure {M : Type u_2} [inst : Monoid M] {A : Type u_1} [inst : Monoid A] {f : M → A} (hf : IsMonoidHom f) (s : Set M) :

f '' Monoid.Closure s = Monoid.Closure (f '' s)

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set under the monoid hom.

theorem AddMonoid.exists_list_of_mem_closure {M : Type u_1} [inst : AddMonoid M] {s : Set M} {a : M} (h : a ∈ AddMonoid.Closure s) :

∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.sum l = a

Given an element a of the AddSubmonoid of an AddMonoid M generated by a set s, there exists a list of elements of s whose sum is a.

theorem Monoid.exists_list_of_mem_closure {M : Type u_1} [inst : Monoid M] {s : Set M} {a : M} (h : a ∈ Monoid.Closure s) :

∃ l, (∀ (x : M), x ∈ l → x ∈ s) ∧ List.prod l = a

Given an element a of the submonoid of a monoid M generated by a set s, there exists a list of elements of s whose product is a.

abbrev AddMonoid.mem_closure_union_iff.match_3 {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} {t : Set M} {x : M} (motive : (∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = x) → Prop) :

(x : ∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = x) → ((y : M) → (hy : y ∈ AddMonoid.Closure s) → (z : M) → (hz : z ∈ AddMonoid.Closure t) → (hyzx : y + z = x) → motive (_ : ∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = x)) → motive x

Equations

One or more equations did not get rendered due to their size.

theorem AddMonoid.mem_closure_union_iff {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} {t : Set M} {x : M} :

x ∈ AddMonoid.Closure (s ∪ t) ↔ ∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = x

Given sets s, t of a commutative AddMonoid M, x ∈ M∈ M is in the AddSubmonoid of M generated by s ∪ t∪ t iff there exists an element of the AddSubmonoid generated by s and an element of the AddSubmonoid generated by t whose sum is x.

abbrev AddMonoid.mem_closure_union_iff.match_1 {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} {t : Set M} (tl : List M) (motive : (∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = List.sum tl) → Prop) :

(x : ∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = List.sum tl) → ((y : M) → (hy : y ∈ AddMonoid.Closure s) → (z : M) → (hz : z ∈ AddMonoid.Closure t) → (hyzx : y + z = List.sum tl) → motive (_ : ∃ y, y ∈ AddMonoid.Closure s ∧ ∃ z, z ∈ AddMonoid.Closure t ∧ y + z = List.sum tl)) → motive x

Equations

One or more equations did not get rendered due to their size.

abbrev AddMonoid.mem_closure_union_iff.match_2 {M : Type u_1} [inst : AddCommMonoid M] {s : Set M} {t : Set M} {x : M} (motive : (∃ l, (∀ (x : M), x ∈ l → x ∈ s ∪ t) ∧ List.sum l = x) → Prop) :

(x : ∃ l, (∀ (x : M), x ∈ l → x ∈ s ∪ t) ∧ List.sum l = x) → ((L : List M) → (HL1 : ∀ (x : M), x ∈ L → x ∈ s ∪ t) → (HL2 : List.sum L = x) → motive (_ : ∃ l, (∀ (x : M), x ∈ l → x ∈ s ∪ t) ∧ List.sum l = x)) → motive x

Equations

AddMonoid.mem_closure_union_iff.match_2 motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem Monoid.mem_closure_union_iff {M : Type u_1} [inst : CommMonoid M] {s : Set M} {t : Set M} {x : M} :

x ∈ Monoid.Closure (s ∪ t) ↔ ∃ y, y ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure t ∧ y * z = x

Given sets s, t of a commutative monoid M, x ∈ M∈ M is in the submonoid of M generated by s ∪ t∪ t iff there exists an element of the submonoid generated by s and an element of the submonoid generated by t whose product is x.

def AddSubmonoid.of.proof_1 {M : Type u_1} [inst : AddMonoid M] {s : Set M} (h : IsAddSubmonoid s) :

∀ (x x_1 : M), x ∈ s → x_1 ∈ s → x + x_1 ∈ s

Equations

(_ : x ∈ s → x ∈ s → x + x ∈ s) = (_ : x ∈ s → x ∈ s → x + x ∈ s)

def AddSubmonoid.of {M : Type u_1} [inst : AddMonoid M] {s : Set M} (h : IsAddSubmonoid s) :

Create a bundled additive submonoid from a set s and [IsAddSubmonoid s].

Equations

AddSubmonoid.of h = { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ (x x_1 : M), x ∈ s → x_1 ∈ s → x + x_1 ∈ s) }, zero_mem' := (_ : 0 ∈ s) }

def Submonoid.of {M : Type u_1} [inst : Monoid M] {s : Set M} (h : IsSubmonoid s) :

Create a bundled submonoid from a set s and [IsSubmonoid s].

Equations

Submonoid.of h = { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ (x x_1 : M), x ∈ s → x_1 ∈ s → x * x_1 ∈ s) }, one_mem' := (_ : 1 ∈ s) }

theorem AddSubmonoid.isAddSubmonoid {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

IsAddSubmonoid ↑S

theorem Submonoid.isSubmonoid {M : Type u_1} [inst : Monoid M] (S : Submonoid M) :

IsSubmonoid ↑S