Documentation

Mathlib.Algebra.Group.Submonoid.Finite

Submonoids #

This file provides some results on multiplicative and additive submonoids in the finite context.

theorem Submonoid.pi_mem_of_mulSingle_mem_aux {η : Type u_1} {f : ηType u_2} [(i : η) → MulOneClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [DecidableEq η] (I : Finset η) {H : S} (x : (i : η) → f i) (h1 : iI, x i = 1) (h2 : iI, Pi.mulSingle i (x i) H) :
x H
theorem AddSubmonoid.pi_mem_of_single_mem_aux {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [DecidableEq η] (I : Finset η) {H : S} (x : (i : η) → f i) (h1 : iI, x i = 0) (h2 : iI, Pi.single i (x i) H) :
x H
theorem Submonoid.pi_mem_of_mulSingle_mem {η : Type u_1} {f : ηType u_2} [(i : η) → MulOneClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [SubmonoidClass S ((i : η) → f i)] [Finite η] [DecidableEq η] {H : S} (x : (i : η) → f i) (h : ∀ (i : η), Pi.mulSingle i (x i) H) :
x H
theorem AddSubmonoid.pi_mem_of_single_mem {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] {S : Type u_3} [SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [Finite η] [DecidableEq η] {H : S} (x : (i : η) → f i) (h : ∀ (i : η), Pi.single i (x i) H) :
x H
theorem Submonoid.pi_le_iff {η : Type u_1} {f : ηType u_2} [(i : η) → MulOneClass (f i)] [Finite η] [DecidableEq η] {H : (i : η) → Submonoid (f i)} {J : Submonoid ((i : η) → f i)} :
pi Set.univ H J ∀ (i : η), map (MonoidHom.mulSingle f i) (H i) J

For finite index types, the Submonoid.pi is generated by the embeddings of the monoids.

theorem AddSubmonoid.pi_le_iff {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] [Finite η] [DecidableEq η] {H : (i : η) → AddSubmonoid (f i)} {J : AddSubmonoid ((i : η) → f i)} :
pi Set.univ H J ∀ (i : η), map (AddMonoidHom.single f i) (H i) J

For finite index types, the Submonoid.pi is generated by the embeddings of the additive monoids.

theorem Submonoid.closure_pi {η : Type u_1} {f : ηType u_2} [(i : η) → MulOneClass (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 1 s i) :
closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)
theorem AddSubmonoid.closure_pi {η : Type u_1} {f : ηType u_2} [(i : η) → AddZeroClass (f i)] [Finite η] {s : (i : η) → Set (f i)} (hs : ∀ (i : η), 0 s i) :
closure (Set.univ.pi fun (i : η) => s i) = pi Set.univ fun (i : η) => closure (s i)