Mathlib.Algebra.Group.Submonoid.BigOperators

SubmonoidClass.coe_list_prod theorem

(l : List S) : (l.prod : M) = (l.map (↑)).prod

Full source

@[to_additive (attr := norm_cast, simp)]
theorem coe_list_prod (l : List S) : (l.prod : M) = (l.map (↑)).prod :=
  map_list_prod (SubmonoidClass.subtype S : _ →* M) l

Coercion of List Product in Submonoid Equals Product of Coerced Elements

Informal description

Let $S$ be a submonoid of a monoid $M$ (i.e., $S$ is closed under multiplication and contains the identity element). For any list $l$ of elements in $S$, the product of $l$ in $S$ (when coerced to $M$) equals the product in $M$ of the elements of $l$ (when each element is coerced to $M$).

SubmonoidClass.coe_multiset_prod theorem

{M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset S) : (m.prod : M) = (m.map (↑)).prod

Full source

@[to_additive (attr := norm_cast, simp)]
theorem coe_multiset_prod {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset S) :
    (m.prod : M) = (m.map (↑)).prod :=
  (SubmonoidClass.subtype S : _ →* M).map_multiset_prod m

Coercion of Multiset Product in Submonoid Equals Product of Coerced Elements

Informal description

Let $M$ be a commutative monoid, $B$ a set-like structure on $M$, and $S$ a submonoid of $M$ (i.e., $S$ is closed under multiplication and contains the identity element). For any multiset $m$ of elements in $S$, the product of $m$ in $S$ (when coerced to $M$) equals the product in $M$ of the elements of $m$ (when each element is coerced to $M$).

SubmonoidClass.coe_finset_prod theorem

 {ι M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ι → S) (s : Finset ι) :
  ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M)

Full source

@[to_additive (attr := norm_cast, simp)]
theorem coe_finset_prod {ι M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (f : ι → S)
    (s : Finset ι) : ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M) :=
  map_prod (SubmonoidClass.subtype S) f s

Coercion of Finite Product in Submonoid Equals Product in Monoid

Informal description

Let $M$ be a commutative monoid, $B$ a set-like structure on $M$, and $S$ a submonoid of $M$. For any function $f \colon \iota \to S$ and any finite set $s \subseteq \iota$, the product $\prod_{i \in s} f i$ in $S$ (when coerced to $M$) equals the product $\prod_{i \in s} f i$ computed directly in $M$.

list_prod_mem theorem

{l : List M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S

Full source

/-- Product of a list of elements in a submonoid is in the submonoid. -/
@[to_additive "Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`."]
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ S) : l.prod ∈ S := by
  lift l to List S using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

Product of Submonoid Elements in a List Belongs to Submonoid

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$. For any list $l$ of elements in $M$, if every element $x \in l$ belongs to $S$, then the product of all elements in $l$ (computed in $M$) also belongs to $S$.

multiset_prod_mem theorem

{M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S

Full source

/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid. -/
@[to_additive
      "Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
      in the `AddSubmonoid`."]
theorem multiset_prod_mem {M} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] (m : Multiset M)
    (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S := by
  lift m to Multiset S using hm
  rw [← coe_multiset_prod]
  exact m.prod.coe_prop

Product of Multiset in Submonoid is in Submonoid

Informal description

Let $M$ be a commutative monoid, $B$ a set-like structure on $M$, and $S$ a submonoid of $M$. For any multiset $m$ of elements in $M$, if every element $a \in m$ belongs to $S$, then the product of all elements in $m$ (computed in $M$) also belongs to $S$.

prod_mem theorem

 {M : Type*} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type*} {t : Finset ι} {f : ι → M}
  (h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S

Full source

/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
    submonoid. -/
@[to_additive
      "Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
      is in the `AddSubmonoid`."]
theorem prod_mem {M : Type*} [CommMonoid M] [SetLike B M] [SubmonoidClass B M] {ι : Type*}
    {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S :=
  multiset_prod_mem (t.1.map f) fun _x hx =>
    let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
    hix ▸ h i hi

Product of Submonoid Elements over a Finite Set Belongs to Submonoid

Informal description

Let $M$ be a commutative monoid, $B$ a set-like structure on $M$, and $S$ a submonoid of $M$. For any finite index set $t$ and function $f : \iota \to M$, if $f(c) \in S$ for every $c \in t$, then the product $\prod_{c \in t} f(c)$ belongs to $S$.

Submonoid.coe_list_prod theorem

(l : List s) : (l.prod : M) = (l.map (↑)).prod

Full source

@[to_additive (attr := norm_cast)]
theorem coe_list_prod (l : List s) : (l.prod : M) = (l.map (↑)).prod :=
  map_list_prod s.subtype l

Product of List in Submonoid Equals Product of Coerced Elements

Informal description

For any list $l$ of elements in a submonoid $S$ of a monoid $M$, the product of $l$ (considered as elements of $M$) is equal to the product of the elements of $l$ when viewed as elements of $M$ via the inclusion map. In other words, if $l = [s_1, \dots, s_n]$ with each $s_i \in S$, then $\prod_{i=1}^n s_i = \prod_{i=1}^n (s_i : M)$.

Submonoid.coe_multiset_prod theorem

{M} [CommMonoid M] (S : Submonoid M) (m : Multiset S) : (m.prod : M) = (m.map (↑)).prod

Full source

@[to_additive (attr := norm_cast)]
theorem coe_multiset_prod {M} [CommMonoid M] (S : Submonoid M) (m : Multiset S) :
    (m.prod : M) = (m.map (↑)).prod :=
  S.subtype.map_multiset_prod m

Product of multiset in submonoid equals product of coerced elements

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any multiset $m$ of elements in $S$, the product of $m$ (considered as elements of $M$) is equal to the product of the elements of $m$ when viewed as elements of $M$ via the inclusion map.

Submonoid.coe_finset_prod theorem

{ι M} [CommMonoid M] (S : Submonoid M) (f : ι → S) (s : Finset ι) : ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M)

Full source

@[to_additive (attr := norm_cast)]
theorem coe_finset_prod {ι M} [CommMonoid M] (S : Submonoid M) (f : ι → S) (s : Finset ι) :
    ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : M) :=
  map_prod S.subtype f s

Inclusion Preserves Finite Products in Submonoids

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any finite set $s$ indexed by a type $\iota$ and any function $f \colon \iota \to S$, the product of $f$ over $s$ (computed in $S$) is equal to the product of $f$ over $s$ when viewed as elements of $M$ via the inclusion map. In other words, the inclusion map preserves finite products.

Submonoid.list_prod_mem theorem

{l : List M} (hl : ∀ x ∈ l, x ∈ s) : l.prod ∈ s

Full source

/-- Product of a list of elements in a submonoid is in the submonoid. -/
@[to_additive "Sum of a list of elements in an `AddSubmonoid` is in the `AddSubmonoid`."]
theorem list_prod_mem {l : List M} (hl : ∀ x ∈ l, x ∈ s) : l.prod ∈ s := by
  lift l to List s using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

Product of List in Submonoid Belongs to Submonoid

Informal description

Let $S$ be a submonoid of a monoid $M$. For any list $l$ of elements in $M$, if every element of $l$ belongs to $S$, then the product of the elements in $l$ (computed in $M$) also belongs to $S$.

Submonoid.multiset_prod_mem theorem

{M} [CommMonoid M] (S : Submonoid M) (m : Multiset M) (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S

Full source

/-- Product of a multiset of elements in a submonoid of a `CommMonoid` is in the submonoid. -/
@[to_additive
      "Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
      in the `AddSubmonoid`."]
theorem multiset_prod_mem {M} [CommMonoid M] (S : Submonoid M) (m : Multiset M)
    (hm : ∀ a ∈ m, a ∈ S) : m.prod ∈ S := by
  lift m to Multiset S using hm
  rw [← coe_multiset_prod]
  exact m.prod.coe_prop

Product of Multiset in Submonoid Belongs to Submonoid

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any multiset $m$ of elements in $M$, if every element of $m$ belongs to $S$, then the product of $m$ (computed in $M$) also belongs to $S$.

Submonoid.multiset_noncommProd_mem theorem

(S : Submonoid M) (m : Multiset M) (comm) (h : ∀ x ∈ m, x ∈ S) : m.noncommProd comm ∈ S

Full source

@[to_additive]
theorem multiset_noncommProd_mem (S : Submonoid M) (m : Multiset M) (comm) (h : ∀ x ∈ m, x ∈ S) :
    m.noncommProd comm ∈ S := by
  induction m using Quotient.inductionOn with | h l => ?_
  simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
  exact Submonoid.list_prod_mem _ h

Noncommutative Product of Commuting Multiset Elements in Submonoid Belongs to Submonoid

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$. For any multiset $m$ of elements in $M$ where all elements pairwise commute, if every element of $m$ belongs to $S$, then the noncommutative product of $m$ (computed in $M$) also belongs to $S$.

Submonoid.prod_mem theorem

 {M : Type*} [CommMonoid M] (S : Submonoid M) {ι : Type*} {t : Finset ι} {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) :
  (∏ c ∈ t, f c) ∈ S

Full source

/-- Product of elements of a submonoid of a `CommMonoid` indexed by a `Finset` is in the
    submonoid. -/
@[to_additive
      "Sum of elements in an `AddSubmonoid` of an `AddCommMonoid` indexed by a `Finset`
      is in the `AddSubmonoid`."]
theorem prod_mem {M : Type*} [CommMonoid M] (S : Submonoid M) {ι : Type*} {t : Finset ι}
    {f : ι → M} (h : ∀ c ∈ t, f c ∈ S) : (∏ c ∈ t, f c) ∈ S :=
  S.multiset_prod_mem (t.1.map f) fun _ hx =>
    let ⟨i, hi, hix⟩ := Multiset.mem_map.1 hx
    hix ▸ h i hi

Product of Finset in Submonoid Belongs to Submonoid

Informal description

Let $M$ be a commutative monoid and $S$ a submonoid of $M$. For any finite index set $I$ and function $f \colon I \to M$, if $f(c) \in S$ for all $c$ in a finite subset $t \subseteq I$, then the product $\prod_{c \in t} f(c)$ belongs to $S$.

Submonoid.noncommProd_mem theorem

 (S : Submonoid M) {ι : Type*} (t : Finset ι) (f : ι → M) (comm) (h : ∀ c ∈ t, f c ∈ S) : t.noncommProd f comm ∈ S

Full source

@[to_additive]
theorem noncommProd_mem (S : Submonoid M) {ι : Type*} (t : Finset ι) (f : ι → M) (comm)
    (h : ∀ c ∈ t, f c ∈ S) : t.noncommProd f comm ∈ S := by
  apply multiset_noncommProd_mem
  intro y
  rw [Multiset.mem_map]
  rintro ⟨x, ⟨hx, rfl⟩⟩
  exact h x hx

Noncommutative Product of Commuting Finset Elements in Submonoid Belongs to Submonoid

Informal description

Let $M$ be a monoid and $S$ a submonoid of $M$. For any finite index set $I$, finite subset $t \subseteq I$, and function $f \colon I \to M$, if all elements of $t$ pairwise commute and $f(c) \in S$ for all $c \in t$, then the noncommutative product $\prod_{c \in t} f(c)$ (computed in $M$) belongs to $S$.

Submonoid.mem_closure_iff_exists_finset_subset theorem

 {s : Set M} : x ∈ closure s ↔ ∃ (f : M → ℕ) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∏ a ∈ t, a ^ f a = x

Full source

@[to_additive]
lemma mem_closure_iff_exists_finset_subset {s : Set M} :
    x ∈ closure sx ∈ closure s ↔
      ∃ (f : M → ℕ) (t : Finset M), ↑t ⊆ s ∧ f.support ⊆ t ∧ ∏ a ∈ t, a ^ f a = x where
  mp hx := by
    classical
    induction hx using closure_induction with
    | one => exact ⟨0, ∅, by simp⟩
    | mem x hx =>
      simp only [Finset.mem_coe] at hx
      exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩
    | mul x y _ _ hx hy =>
    obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]
  mpr := by
    rintro ⟨n, t, hts, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure <| hts hx) _

Characterization of Submonoid Membership via Finite Exponents and Products

Informal description

Let $M$ be a monoid and $s$ a subset of $M$. An element $x \in M$ belongs to the submonoid generated by $s$ if and only if there exists a function $f \colon M \to \mathbb{N}$ and a finite subset $t \subseteq s$ such that: 1. The support of $f$ is contained in $t$, and 2. $x$ can be expressed as the product $\prod_{a \in t} a^{f(a)}$.

Submonoid.mem_closure_finset theorem

{s : Finset M} : x ∈ closure s ↔ ∃ f : M → ℕ, f.support ⊆ s ∧ ∏ a ∈ s, a ^ f a = x

Full source

@[to_additive]
lemma mem_closure_finset {s : Finset M} :
    x ∈ closure sx ∈ closure s ↔ ∃ f : M → ℕ, f.support ⊆ s ∧ ∏ a ∈ s, a ^ f a = x where
  mp := by
    rw [mem_closure_iff_exists_finset_subset]
    rintro ⟨f, t, hts, hf, rfl⟩
    refine ⟨f, hf.trans hts, .symm <| Finset.prod_subset hts ?_⟩
    simp +contextual [Function.support_subset_iff'.1 hf]
  mpr := by rintro ⟨n, -, rfl⟩; exact prod_mem _ fun x hx ↦ pow_mem (subset_closure hx) _

Characterization of Submonoid Membership via Finite Exponents and Products for Finite Generating Sets

Informal description

Let $M$ be a monoid and $s$ a finite subset of $M$. An element $x \in M$ belongs to the submonoid generated by $s$ if and only if there exists a function $f \colon M \to \mathbb{N}$ such that: 1. The support of $f$ is contained in $s$, and 2. $x$ can be expressed as the product $\prod_{a \in s} a^{f(a)}$.

Tags