Documentation

Mathlib.GroupTheory.Submonoid.Basic

Submonoids: definition and `CompleteLattice` structure #

This file defines bundled multiplicative and additive submonoids. We also define a CompleteLattice structure on Submonoids, define the closure of a set as the minimal submonoid that includes this set, and prove a few results about extending properties from a dense set (i.e. a set with closure s = ⊤⊤) to the whole monoid, see Submonoid.dense_induction and MonoidHom.ofClosureEqTopLeft/MonoidHom.ofClosureEqTopRight.

Main definitions #

Submonoid M: the type of bundled submonoids of a monoid M; the underlying set is given in the carrier field of the structure, and should be accessed through coercion as in (S : Set M).
AddSubmonoid M : the type of bundled submonoids of an additive monoid M.

For each of the following definitions in the Submonoid namespace, there is a corresponding definition in the AddSubmonoid namespace.

Submonoid.copy : copy of a submonoid with carrier replaced by a set that is equal but possibly not definitionally equal to the carrier of the original Submonoid.
Submonoid.closure : monoid closure of a set, i.e., the least submonoid that includes the set.
Submonoid.gi : closure : Set M → Submonoid M→ Submonoid M and coercion coe : Submonoid M → Set M→ Set M form a GaloisInsertion;
MonoidHom.eqLocus: the submonoid of elements x : M such that f x = g x;
MonoidHom.ofClosureEqTopRight: if a map f : M → N→ N between two monoids satisfies f 1 = 1 and f (x * y) = f x * f y for y from some dense set s, then f is a monoid homomorphism. E.g., if f : ℕ → M→ M satisfies f 0 = 0 and f (x + 1) = f x + f 1, then f is an additive monoid homomorphism.

Implementation notes #

Submonoid inclusion is denoted ≤≤ rather than ⊆⊆, although ∈∈ is defined as membership of a submonoid's underlying set.

Note that Submonoid M does not actually require Monoid M, instead requiring only the weaker MulOneClass M.

This file is designed to have very few dependencies. In particular, it should not use natural numbers. Submonoid is implemented by extending Subsemigroup requiring one_mem'.

Tags #

submonoid, submonoids

class OneMemClass (S : Type u_1) (M : Type u_2) [inst : One M] [inst : SetLike S M] :

By definition, if we have OneMemClass S M, we have 1 ∈ s∈ s for all s : S.
one_mem : ∀ (s : S), 1 ∈ s

OneMemClass S M says S is a type of subsets s ≤ M≤ M, such that 1 ∈ s∈ s for all s.

Instances

class ZeroMemClass (S : Type u_1) (M : Type u_2) [inst : Zero M] [inst : SetLike S M] :

By definition, if we have ZeroMemClass S M, we have 0 ∈ s∈ s for all s : S.
zero_mem : ∀ (s : S), 0 ∈ s

ZeroMemClass S M says S is a type of subsets s ≤ M≤ M, such that 0 ∈ s∈ s for all s.

Instances

structure Submonoid (M : Type u_1) [inst : MulOneClass M] extends Subsemigroup :

Type u_1

A submonoid contains 1.
one_mem' : 1 ∈ toSubsemigroup.carrier

A submonoid of a monoid M is a subset containing 1 and closed under multiplication.

Instances For

class SubmonoidClass (S : Type u_1) (M : Type u_2) [inst : MulOneClass M] [inst : SetLike S M] extends MulMemClass , OneMemClass :

SubmonoidClass S M says S is a type of subsets s ≤ M≤ M that contain 1 and are closed under (*)

Instances

structure AddSubmonoid (M : Type u_1) [inst : AddZeroClass M] extends AddSubsemigroup :

Type u_1

An additive submonoid contains 0.
zero_mem' : 0 ∈ toAddSubsemigroup.carrier

An additive submonoid of an additive monoid M is a subset containing 0 and closed under addition.

Instances For

class AddSubmonoidClass (S : Type u_1) (M : Type u_2) [inst : AddZeroClass M] [inst : SetLike S M] extends AddMemClass , ZeroMemClass :

AddSubmonoidClass S M says S is a type of subsets s ≤ M≤ M that contain 0 and are closed under (+)

Instances

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

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

Equations

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

theorem nsmul_mem {M : Type u_1} {A : Type u_2} [inst : AddMonoid M] [inst : SetLike A M] [inst : AddSubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) :

n • x ∈ S

theorem pow_mem {M : Type u_1} {A : Type u_2} [inst : Monoid M] [inst : SetLike A M] [inst : SubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) :

x ^ n ∈ S

def AddSubmonoid.instSetLikeAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] (p : AddSubmonoid M) (q : AddSubmonoid M) (h : (fun s => s.toAddSubsemigroup.carrier) p = (fun s => s.toAddSubsemigroup.carrier) q) :

p = q

Equations

(_ : p = q) = (_ : p = q)

instance AddSubmonoid.instSetLikeAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

SetLike (AddSubmonoid M) M

Equations

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

instance Submonoid.instSetLikeSubmonoid {M : Type u_1} [inst : MulOneClass M] :

SetLike (Submonoid M) M

Equations

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

instance AddSubmonoid.instAddSubmonoidClassAddSubmonoidInstSetLikeAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

AddSubmonoidClass (AddSubmonoid M) M

Equations

@AddSubmonoid.instAddSubmonoidClassAddSubmonoidInstSetLikeAddSubmonoid = @AddSubmonoid.instAddSubmonoidClassAddSubmonoidInstSetLikeAddSubmonoid.proof_1

def AddSubmonoid.instAddSubmonoidClassAddSubmonoidInstSetLikeAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] :

AddSubmonoidClass (AddSubmonoid M) M

Equations

(_ : AddSubmonoidClass (AddSubmonoid M) M) = (_ : AddSubmonoidClass (AddSubmonoid M) M)

instance Submonoid.instSubmonoidClassSubmonoidInstSetLikeSubmonoid {M : Type u_1} [inst : MulOneClass M] :

SubmonoidClass (Submonoid M) M

Equations

@Submonoid.instSubmonoidClassSubmonoidInstSetLikeSubmonoid = @Submonoid.instSubmonoidClassSubmonoidInstSetLikeSubmonoid.proof_1

@[simp]

theorem AddSubmonoid.mem_toSubsemigroup {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {x : M} :

x ∈ s.toAddSubsemigroup ↔ x ∈ s

@[simp]

theorem Submonoid.mem_toSubsemigroup {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {x : M} :

x ∈ s.toSubsemigroup ↔ x ∈ s

theorem AddSubmonoid.mem_carrier {M : Type u_1} [inst : AddZeroClass M] {s : AddSubmonoid M} {x : M} :

x ∈ s.toAddSubsemigroup.carrier ↔ x ∈ s

theorem Submonoid.mem_carrier {M : Type u_1} [inst : MulOneClass M] {s : Submonoid M} {x : M} :

x ∈ s.toSubsemigroup.carrier ↔ x ∈ s

@[simp]

theorem AddSubmonoid.mem_mk {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {x : M} (h_one : s 0) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :

x ∈ { toAddSubsemigroup := { carrier := s, add_mem' := h_mul }, zero_mem' := h_one } ↔ x ∈ s

@[simp]

theorem Submonoid.mem_mk {M : Type u_1} [inst : MulOneClass M] {s : Set M} {x : M} (h_one : s 1) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :

x ∈ { toSubsemigroup := { carrier := s, mul_mem' := h_mul }, one_mem' := h_one } ↔ x ∈ s

@[simp]

theorem AddSubmonoid.coe_set_mk {M : Type u_1} [inst : AddZeroClass M] {s : Set M} (h_one : s 0) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) :

↑{ toAddSubsemigroup := { carrier := s, add_mem' := h_mul }, zero_mem' := h_one } = s

@[simp]

theorem Submonoid.coe_set_mk {M : Type u_1} [inst : MulOneClass M] {s : Set M} (h_one : s 1) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) :

↑{ toSubsemigroup := { carrier := s, mul_mem' := h_mul }, one_mem' := h_one } = s

@[simp]

theorem AddSubmonoid.mk_le_mk {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {t : Set M} (h_one : s 0) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) (h_one' : t 0) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a + b ∈ t) :

{ toAddSubsemigroup := { carrier := s, add_mem' := h_mul }, zero_mem' := h_one } ≤ { toAddSubsemigroup := { carrier := t, add_mem' := h_mul' }, zero_mem' := h_one' } ↔ s ⊆ t

@[simp]

theorem Submonoid.mk_le_mk {M : Type u_1} [inst : MulOneClass M] {s : Set M} {t : Set M} (h_one : s 1) (h_mul : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) (h_one' : t 1) (h_mul' : ∀ {a b : M}, a ∈ t → b ∈ t → a * b ∈ t) :

{ toSubsemigroup := { carrier := s, mul_mem' := h_mul }, one_mem' := h_one } ≤ { toSubsemigroup := { carrier := t, mul_mem' := h_mul' }, one_mem' := h_one' } ↔ s ⊆ t

theorem AddSubmonoid.ext {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :

S = T

Two AddSubmonoids are equal if they have the same elements.

theorem Submonoid.ext {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : ∀ (x : M), x ∈ S ↔ x ∈ T) :

S = T

Two submonoids are equal if they have the same elements.

def AddSubmonoid.copy.proof_2 {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = ↑S) :

0 ∈ s

Equations

(_ : 0 ∈ s) = (_ : 0 ∈ s)

def AddSubmonoid.copy {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = ↑S) :

Copy an additive submonoid replacing carrier with a set that is equal to it.

Equations

AddSubmonoid.copy S s hs = { toAddSubsemigroup := { carrier := s, add_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s) }, zero_mem' := (_ : 0 ∈ s) }

def AddSubmonoid.copy.proof_1 {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = ↑S) :

∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

Equations

(_ : a ∈ s → b ∈ s → a + b ∈ s) = (_ : a ∈ s → b ∈ s → a + b ∈ s)

def Submonoid.copy {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) (s : Set M) (hs : s = ↑S) :

Copy a submonoid replacing carrier with a set that is equal to it.

Equations

Submonoid.copy S s hs = { toSubsemigroup := { carrier := s, mul_mem' := (_ : ∀ {a b : M}, a ∈ s → b ∈ s → a * b ∈ s) }, one_mem' := (_ : 1 ∈ s) }

@[simp]

theorem AddSubmonoid.coe_copy {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = ↑S) :

↑(AddSubmonoid.copy S s hs) = s

@[simp]

theorem Submonoid.coe_copy {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = ↑S) :

↑(Submonoid.copy S s hs) = s

theorem AddSubmonoid.copy_eq {M : Type u_1} [inst : AddZeroClass M] {S : AddSubmonoid M} {s : Set M} (hs : s = ↑S) :

AddSubmonoid.copy S s hs = S

theorem Submonoid.copy_eq {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = ↑S) :

Submonoid.copy S s hs = S

theorem AddSubmonoid.zero_mem {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

0 ∈ S

An AddSubmonoid contains the monoid's 0.

theorem Submonoid.one_mem {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

1 ∈ S

A submonoid contains the monoid's 1.

theorem AddSubmonoid.add_mem {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) {x : M} {y : M} :

x ∈ S → y ∈ S → x + y ∈ S

An AddSubmonoid is closed under addition.

theorem Submonoid.mul_mem {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) {x : M} {y : M} :

x ∈ S → y ∈ S → x * y ∈ S

A submonoid is closed under multiplication.

instance AddSubmonoid.instTopAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

Top (AddSubmonoid M)

The additive submonoid M of the AddMonoid M.

Equations

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

def AddSubmonoid.instTopAddSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] :

0 ∈ Set.univ

Equations

(_ : 0 ∈ Set.univ) = (_ : 0 ∈ Set.univ)

def AddSubmonoid.instTopAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] :

∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a + b ∈ Set.univ

Equations

(_ : a + b ∈ Set.univ) = (_ : a + b ∈ Set.univ)

instance Submonoid.instTopSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Top (Submonoid M)

The submonoid M of the monoid M.

Equations

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

instance AddSubmonoid.instBotAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

Bot (AddSubmonoid M)

The trivial AddSubmonoid {0} of an AddMonoid M.

Equations

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

def AddSubmonoid.instBotAddSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] :

0 ∈ {0}

Equations

(_ : 0 ∈ {0}) = (_ : 0 ∈ {0})

def AddSubmonoid.instBotAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] :

∀ {a b : M}, a ∈ {0} → b ∈ {0} → a + b ∈ {0}

Equations

(_ : a + b ∈ {0}) = (_ : a + b ∈ {0})

instance Submonoid.instBotSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Bot (Submonoid M)

The trivial submonoid {1} of an monoid M.

Equations

Submonoid.instBotSubmonoid = { bot := { toSubsemigroup := { carrier := {1}, mul_mem' := (_ : ∀ {a b : M}, a ∈ {1} → b ∈ {1} → a * b ∈ {1}) }, one_mem' := (_ : 1 ∈ {1}) } }

instance AddSubmonoid.instInhabitedAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

Inhabited (AddSubmonoid M)

Equations

AddSubmonoid.instInhabitedAddSubmonoid = { default := ⊥ }

instance Submonoid.instInhabitedSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Inhabited (Submonoid M)

Equations

Submonoid.instInhabitedSubmonoid = { default := ⊥ }

@[simp]

theorem AddSubmonoid.mem_bot {M : Type u_1} [inst : AddZeroClass M] {x : M} :

x ∈ ⊥ ↔ x = 0

@[simp]

theorem Submonoid.mem_bot {M : Type u_1} [inst : MulOneClass M] {x : M} :

x ∈ ⊥ ↔ x = 1

@[simp]

theorem AddSubmonoid.mem_top {M : Type u_1} [inst : AddZeroClass M] (x : M) :

@[simp]

theorem Submonoid.mem_top {M : Type u_1} [inst : MulOneClass M] (x : M) :

@[simp]

theorem AddSubmonoid.coe_top {M : Type u_1} [inst : AddZeroClass M] :

↑⊤ = Set.univ

@[simp]

theorem Submonoid.coe_top {M : Type u_1} [inst : MulOneClass M] :

↑⊤ = Set.univ

@[simp]

theorem AddSubmonoid.coe_bot {M : Type u_1} [inst : AddZeroClass M] :

↑⊥ = {0}

@[simp]

theorem Submonoid.coe_bot {M : Type u_1} [inst : MulOneClass M] :

↑⊥ = {1}

abbrev AddSubmonoid.instInfAddSubmonoid.match_1 {M : Type u_1} [inst : AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :

{b : M} → ∀ (motive : b ∈ ↑S₁ ∩ ↑S₂ → Prop) (x : b ∈ ↑S₁ ∩ ↑S₂), (∀ (hy : b ∈ ↑S₁) (hy' : b ∈ ↑S₂), motive (_ : b ∈ ↑S₁ ∧ b ∈ ↑S₂)) → motive x

Equations

AddSubmonoid.instInfAddSubmonoid.match_1 S₁ S₂ motive x h_1 = And.casesOn x fun left right => h_1 left right

instance AddSubmonoid.instInfAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

Inf (AddSubmonoid M)

The inf of two AddSubmonoids is their intersection.

Equations

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

def AddSubmonoid.instInfAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :

∀ {a b : M}, a ∈ ↑S₁ ∩ ↑S₂ → b ∈ ↑S₁ ∩ ↑S₂ → a + b ∈ ↑S₁ ∩ ↑S₂

Equations

(_ : a + b ∈ ↑S₁ ∩ ↑S₂) = (_ : a + b ∈ ↑S₁ ∩ ↑S₂)

def AddSubmonoid.instInfAddSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) :

0 ∈ ↑S₁ ∧ 0 ∈ ↑S₂

Equations

(_ : 0 ∈ ↑S₁ ∧ 0 ∈ ↑S₂) = (_ : 0 ∈ ↑S₁ ∧ 0 ∈ ↑S₂)

instance Submonoid.instInfSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Inf (Submonoid M)

The inf of two submonoids is their intersection.

Equations

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

@[simp]

theorem AddSubmonoid.coe_inf {M : Type u_1} [inst : AddZeroClass M] (p : AddSubmonoid M) (p' : AddSubmonoid M) :

↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Submonoid.coe_inf {M : Type u_1} [inst : MulOneClass M] (p : Submonoid M) (p' : Submonoid M) :

↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubmonoid.mem_inf {M : Type u_1} [inst : AddZeroClass M] {p : AddSubmonoid M} {p' : AddSubmonoid M} {x : M} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem Submonoid.mem_inf {M : Type u_1} [inst : MulOneClass M] {p : Submonoid M} {p' : Submonoid M} {x : M} :

x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

instance AddSubmonoid.instInfSetAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

InfSet (AddSubmonoid M)

Equations

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

def AddSubmonoid.instInfSetAddSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) :

0 ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x

Equations

(_ : 0 ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : 0 ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)

def AddSubmonoid.instInfSetAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) :

∀ {a b : M}, (a ∈ Set.interᵢ fun t => Set.interᵢ fun h => ↑t) → (b ∈ Set.interᵢ fun t => Set.interᵢ fun h => ↑t) → a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x

Equations

(_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x) = (_ : a + b ∈ Set.interᵢ fun x => Set.interᵢ fun h => ↑x)

instance Submonoid.instInfSetSubmonoid {M : Type u_1} [inst : MulOneClass M] :

InfSet (Submonoid M)

Equations

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

@[simp]

theorem AddSubmonoid.coe_infₛ {M : Type u_1} [inst : AddZeroClass M] (S : Set (AddSubmonoid M)) :

↑(infₛ S) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

@[simp]

theorem Submonoid.coe_infₛ {M : Type u_1} [inst : MulOneClass M] (S : Set (Submonoid M)) :

↑(infₛ S) = Set.interᵢ fun s => Set.interᵢ fun h => ↑s

theorem AddSubmonoid.mem_infₛ {M : Type u_1} [inst : AddZeroClass M] {S : Set (AddSubmonoid M)} {x : M} :

x ∈ infₛ S ↔ ∀ (p : AddSubmonoid M), p ∈ S → x ∈ p

theorem Submonoid.mem_infₛ {M : Type u_1} [inst : MulOneClass M] {S : Set (Submonoid M)} {x : M} :

x ∈ infₛ S ↔ ∀ (p : Submonoid M), p ∈ S → x ∈ p

theorem AddSubmonoid.mem_infᵢ {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} {S : ι → AddSubmonoid M} {x : M} :

(x ∈ ⨅ i, S i) ↔ ∀ (i : ι), x ∈ S i

theorem Submonoid.mem_infᵢ {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} {S : ι → Submonoid M} {x : M} :

(x ∈ ⨅ i, S i) ↔ ∀ (i : ι), x ∈ S i

@[simp]

theorem AddSubmonoid.coe_infᵢ {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} {S : ι → AddSubmonoid M} :

↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

@[simp]

theorem Submonoid.coe_infᵢ {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} {S : ι → Submonoid M} :

↑(⨅ i, S i) = Set.interᵢ fun i => ↑(S i)

instance AddSubmonoid.instCompleteLatticeAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] :

CompleteLattice (AddSubmonoid M)

The AddSubmonoids of an AddMonoid form a complete lattice.

Equations

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

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_9 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x x_1 : AddSubmonoid M) (x_2 : M), x_2 ∈ ↑x ∧ x_2 ∈ ↑x_1 → x_2 ∈ ↑x

Equations

(_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_8 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) (c : AddSubmonoid M) :

a ≤ c → b ≤ c → a ⊔ b ≤ c

Equations

(_ : ∀ (a b c : AddSubmonoid M), a ≤ c → b ≤ c → a ⊔ b ≤ c) = (_ : ∀ (a b c : AddSubmonoid M), a ≤ c → b ≤ c → a ⊔ b ≤ c)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_7 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) :

b ≤ a ⊔ b

Equations

(_ : ∀ (a b : AddSubmonoid M), b ≤ a ⊔ b) = (_ : ∀ (a b : AddSubmonoid M), b ≤ a ⊔ b)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_16 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x : AddSubmonoid M) (x_1 : M), x_1 ∈ x → x_1 ∈ ⊤

Equations

(_ : x ∈ ⊤) = (_ : x ∈ ⊤)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_2 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) :

a ≤ a

Equations

(_ : ∀ (a : AddSubmonoid M), a ≤ a) = (_ : ∀ (a : AddSubmonoid M), a ≤ a)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_6 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) :

a ≤ a ⊔ b

Equations

(_ : ∀ (a b : AddSubmonoid M), a ≤ a ⊔ b) = (_ : ∀ (a b : AddSubmonoid M), a ≤ a ⊔ b)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_4 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) :

a < b ↔ a ≤ b ∧ ¬b ≤ a

Equations

(_ : ∀ (a b : AddSubmonoid M), a < b ↔ a ≤ b ∧ ¬b ≤ a) = (_ : ∀ (a b : AddSubmonoid M), a < b ↔ a ≤ b ∧ ¬b ≤ a)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_3 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) (c : AddSubmonoid M) :

a ≤ b → b ≤ c → a ≤ c

Equations

(_ : ∀ (a b c : AddSubmonoid M), a ≤ b → b ≤ c → a ≤ c) = (_ : ∀ (a b c : AddSubmonoid M), a ≤ b → b ≤ c → a ≤ c)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_14 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :

a ∈ s → infₛ s ≤ a

Equations

(_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → infₛ s ≤ a) = (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → infₛ s ≤ a)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_10 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x x_1 : AddSubmonoid M) (x_2 : M), x_2 ∈ ↑x ∧ x_2 ∈ ↑x_1 → x_2 ∈ ↑x_1

Equations

(_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x → x ∈ ↑x)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_12 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :

a ∈ s → a ≤ supₛ s

Equations

(_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → a ≤ supₛ s) = (_ : ∀ (s : Set (AddSubmonoid M)) (a : AddSubmonoid M), a ∈ s → a ≤ supₛ s)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_5 {M : Type u_1} [inst : AddZeroClass M] (a : AddSubmonoid M) (b : AddSubmonoid M) :

a ≤ b → b ≤ a → a = b

Equations

(_ : ∀ (a b : AddSubmonoid M), a ≤ b → b ≤ a → a = b) = (_ : ∀ (a b : AddSubmonoid M), a ≤ b → b ≤ a → a = b)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x : Set (AddSubmonoid M)), IsGLB x (infₛ x)

Equations

(_ : IsGLB x (infₛ x)) = (_ : IsGLB x (infₛ x))

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_13 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :

(∀ (b : AddSubmonoid M), b ∈ s → b ≤ a) → supₛ s ≤ a

Equations

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

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_15 {M : Type u_1} [inst : AddZeroClass M] (s : Set (AddSubmonoid M)) (a : AddSubmonoid M) :

(∀ (b : AddSubmonoid M), b ∈ s → a ≤ b) → a ≤ infₛ s

Equations

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

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_11 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x x_1 x_2 : AddSubmonoid M), x ≤ x_1 → x ≤ x_2 → ∀ (x_3 : M), x_3 ∈ x → x_3 ∈ ↑x_1 ∧ x_3 ∈ ↑x_2

Equations

(_ : x ∈ ↑x ∧ x ∈ ↑x) = (_ : x ∈ ↑x ∧ x ∈ ↑x)

def AddSubmonoid.instCompleteLatticeAddSubmonoid.proof_17 {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

∀ (x : M), x ∈ ⊥ → x ∈ S

Equations

(_ : x ∈ S) = (_ : x ∈ S)

instance Submonoid.instCompleteLatticeSubmonoid {M : Type u_1} [inst : MulOneClass M] :

CompleteLattice (Submonoid M)

Submonoids of a monoid form a complete lattice.

Equations

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

@[simp]

theorem AddSubmonoid.subsingleton_iff {M : Type u_1} [inst : AddZeroClass M] :

Subsingleton (AddSubmonoid M) ↔ Subsingleton M

@[simp]

theorem Submonoid.subsingleton_iff {M : Type u_1} [inst : MulOneClass M] :

Subsingleton (Submonoid M) ↔ Subsingleton M

@[simp]

theorem AddSubmonoid.nontrivial_iff {M : Type u_1} [inst : AddZeroClass M] :

Nontrivial (AddSubmonoid M) ↔ Nontrivial M

@[simp]

theorem Submonoid.nontrivial_iff {M : Type u_1} [inst : MulOneClass M] :

Nontrivial (Submonoid M) ↔ Nontrivial M

instance AddSubmonoid.instUniqueAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] [inst : Subsingleton M] :

Unique (AddSubmonoid M)

Equations

AddSubmonoid.instUniqueAddSubmonoid = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (a : AddSubmonoid M), a = default) }

def AddSubmonoid.instUniqueAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] [inst : Subsingleton M] (a : AddSubmonoid M) :

a = default

Equations

(_ : a = default) = (_ : a = default)

instance Submonoid.instUniqueSubmonoid {M : Type u_1} [inst : MulOneClass M] [inst : Subsingleton M] :

Unique (Submonoid M)

Equations

Submonoid.instUniqueSubmonoid = { toInhabited := { default := ⊥ }, uniq := (_ : ∀ (a : Submonoid M), a = default) }

instance AddSubmonoid.instNontrivialAddSubmonoid {M : Type u_1} [inst : AddZeroClass M] [inst : Nontrivial M] :

Nontrivial (AddSubmonoid M)

Equations

@AddSubmonoid.instNontrivialAddSubmonoid = @AddSubmonoid.instNontrivialAddSubmonoid.proof_1

def AddSubmonoid.instNontrivialAddSubmonoid.proof_1 {M : Type u_1} [inst : AddZeroClass M] [inst : Nontrivial M] :

Nontrivial (AddSubmonoid M)

Equations

(_ : Nontrivial (AddSubmonoid M)) = (_ : Nontrivial (AddSubmonoid M))

instance Submonoid.instNontrivialSubmonoid {M : Type u_1} [inst : MulOneClass M] [inst : Nontrivial M] :

Nontrivial (Submonoid M)

Equations

@Submonoid.instNontrivialSubmonoid = @Submonoid.instNontrivialSubmonoid.proof_1

def AddSubmonoid.closure {M : Type u_1} [inst : AddZeroClass M] (s : Set M) :

The add_submonoid generated by a set

Equations

AddSubmonoid.closure s = infₛ { S | s ⊆ ↑S }

def Submonoid.closure {M : Type u_1} [inst : MulOneClass M] (s : Set M) :

The Submonoid generated by a set.

Equations

Submonoid.closure s = infₛ { S | s ⊆ ↑S }

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

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

@[simp]

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

s ⊆ ↑(AddSubmonoid.closure s)

The AddSubmonoid generated by a set includes the set.

@[simp]

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

s ⊆ ↑(Submonoid.closure s)

The submonoid generated by a set includes the set.

theorem AddSubmonoid.not_mem_of_not_mem_closure {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {P : M} (hP : ¬P ∈ AddSubmonoid.closure s) :

theorem Submonoid.not_mem_of_not_mem_closure {M : Type u_1} [inst : MulOneClass M] {s : Set M} {P : M} (hP : ¬P ∈ Submonoid.closure s) :

@[simp]

theorem AddSubmonoid.closure_le {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M} :

AddSubmonoid.closure s ≤ S ↔ s ⊆ ↑S

An additive submonoid S includes closure s if and only if it includes s

@[simp]

theorem Submonoid.closure_le {M : Type u_1} [inst : MulOneClass M] {s : Set M} {S : Submonoid M} :

Submonoid.closure s ≤ S ↔ s ⊆ ↑S

A submonoid S includes closure s if and only if it includes s.

theorem AddSubmonoid.closure_mono {M : Type u_1} [inst : AddZeroClass M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) :

AddSubmonoid.closure s ≤ AddSubmonoid.closure t

Additive submonoid closure of a set is monotone in its argument: if s ⊆ t⊆ t, then closure s ≤ closure t≤ closure t

theorem Submonoid.closure_mono {M : Type u_1} [inst : MulOneClass M] ⦃s : Set M⦄ ⦃t : Set M⦄ (h : s ⊆ t) :

Submonoid.closure s ≤ Submonoid.closure t

Submonoid closure of a set is monotone in its argument: if s ⊆ t⊆ t, then closure s ≤ closure t≤ closure t.

theorem AddSubmonoid.closure_eq_of_le {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {S : AddSubmonoid M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ AddSubmonoid.closure s) :

AddSubmonoid.closure s = S

theorem Submonoid.closure_eq_of_le {M : Type u_1} [inst : MulOneClass M] {s : Set M} {S : Submonoid M} (h₁ : s ⊆ ↑S) (h₂ : S ≤ Submonoid.closure s) :

Submonoid.closure s = S

theorem AddSubmonoid.closure_induction {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ AddSubmonoid.closure s) (Hs : (x : M) → x ∈ s → p x) (H1 : p 0) (Hmul : (x y : M) → p x → p y → p (x + y)) :

p x

An induction principle for additive closure membership. If p holds for 0 and all elements of s, and is preserved under addition, then p holds for all elements of the additive closure of s.

theorem Submonoid.closure_induction {M : Type u_1} [inst : MulOneClass M] {s : Set M} {p : M → Prop} {x : M} (h : x ∈ Submonoid.closure s) (Hs : (x : M) → x ∈ s → p x) (H1 : p 1) (Hmul : (x y : M) → p x → p y → p (x * y)) :

p x

An induction principle for closure membership. If p holds for 1 and all elements of s, and is preserved under multiplication, then p holds for all elements of the closure of s.

theorem AddSubmonoid.closure_induction' {M : Type u_1} [inst : AddZeroClass M] (s : Set M) {p : (x : M) → x ∈ AddSubmonoid.closure s → Prop} (Hs : (x : M) → (h : x ∈ s) → p x (_ : x ∈ ↑(AddSubmonoid.closure s))) (H1 : p 0 (_ : 0 ∈ AddSubmonoid.closure s)) (Hmul : (x : M) → (hx : x ∈ AddSubmonoid.closure s) → (y : M) → (hy : y ∈ AddSubmonoid.closure s) → p x hx → p y hy → p (x + y) (_ : x + y ∈ AddSubmonoid.closure s)) {x : M} (hx : x ∈ AddSubmonoid.closure s) :

p x hx

A dependent version of AddSubmonoid.closure_induction.

abbrev AddSubmonoid.closure_induction'.match_1 {M : Type u_1} [inst : AddZeroClass M] (s : Set M) {p : (x : M) → x ∈ AddSubmonoid.closure s → Prop} (y : M) (motive : (∃ x, p y x) → Prop) :

(x : ∃ x, p y x) → ((hy' : y ∈ AddSubmonoid.closure s) → (hy : p y hy') → motive (_ : ∃ x, p y x)) → motive x

Equations

AddSubmonoid.closure_induction'.match_1 s y motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem Submonoid.closure_induction' {M : Type u_1} [inst : MulOneClass M] (s : Set M) {p : (x : M) → x ∈ Submonoid.closure s → Prop} (Hs : (x : M) → (h : x ∈ s) → p x (_ : x ∈ ↑(Submonoid.closure s))) (H1 : p 1 (_ : 1 ∈ Submonoid.closure s)) (Hmul : (x : M) → (hx : x ∈ Submonoid.closure s) → (y : M) → (hy : y ∈ Submonoid.closure s) → p x hx → p y hy → p (x * y) (_ : x * y ∈ Submonoid.closure s)) {x : M} (hx : x ∈ Submonoid.closure s) :

p x hx

A dependent version of Submonoid.closure_induction.

theorem AddSubmonoid.closure_induction₂ {M : Type u_1} [inst : AddZeroClass M] {s : Set M} {p : M → M → Prop} {x : M} {y : M} (hx : x ∈ AddSubmonoid.closure s) (hy : y ∈ AddSubmonoid.closure s) (Hs : (x : M) → x ∈ s → (y : M) → y ∈ s → p x y) (H1_left : (x : M) → p 0 x) (H1_right : (x : M) → p x 0) (Hmul_left : (x y z : M) → p x z → p y z → p (x + y) z) (Hmul_right : (x y z : M) → p z x → p z y → p z (x + y)) :

p x y

An induction principle for additive closure membership for predicates with two arguments.

theorem Submonoid.closure_induction₂ {M : Type u_1} [inst : MulOneClass M] {s : Set M} {p : M → M → Prop} {x : M} {y : M} (hx : x ∈ Submonoid.closure s) (hy : y ∈ Submonoid.closure s) (Hs : (x : M) → x ∈ s → (y : M) → y ∈ s → p x y) (H1_left : (x : M) → p 1 x) (H1_right : (x : M) → p x 1) (Hmul_left : (x y z : M) → p x z → p y z → p (x * y) z) (Hmul_right : (x y z : M) → p z x → p z y → p z (x * y)) :

p x y

An induction principle for closure membership for predicates with two arguments.

theorem AddSubmonoid.dense_induction {M : Type u_1} [inst : AddZeroClass M] {p : M → Prop} (x : M) {s : Set M} (hs : AddSubmonoid.closure s = ⊤) (Hs : (x : M) → x ∈ s → p x) (H1 : p 0) (Hmul : (x y : M) → p x → p y → p (x + y)) :

p x

If s is a dense set in an additive monoid M, AddSubmonoid.closure s = ⊤⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s∈ s, verify p 0, and verify that p x and p y imply p (x + y).

theorem Submonoid.dense_induction {M : Type u_1} [inst : MulOneClass M] {p : M → Prop} (x : M) {s : Set M} (hs : Submonoid.closure s = ⊤) (Hs : (x : M) → x ∈ s → p x) (H1 : p 1) (Hmul : (x y : M) → p x → p y → p (x * y)) :

p x

If s is a dense set in a monoid M, Submonoid.closure s = ⊤⊤, then in order to prove that some predicate p holds for all x : M it suffices to verify p x for x ∈ s∈ s, verify p 1, and verify that p x and p y imply p (x * y).

def AddSubmonoid.gi.proof_2 (M : Type u_1) [inst : AddZeroClass M] :

∀ (x : AddSubmonoid M), ↑x ⊆ ↑(AddSubmonoid.closure ↑x)

Equations

(_ : ↑x ⊆ ↑(AddSubmonoid.closure ↑x)) = (_ : ↑x ⊆ ↑(AddSubmonoid.closure ↑x))

def AddSubmonoid.gi.proof_1 (M : Type u_1) [inst : AddZeroClass M] :

∀ (x : Set M) (x_1 : AddSubmonoid M), AddSubmonoid.closure x ≤ x_1 ↔ x ⊆ ↑x_1

Equations

(_ : AddSubmonoid.closure x ≤ x ↔ x ⊆ ↑x) = (_ : AddSubmonoid.closure x ≤ x ↔ x ⊆ ↑x)

def AddSubmonoid.gi.proof_3 (M : Type u_1) [inst : AddZeroClass M] :

∀ (x : Set M) (x_1 : ↑(AddSubmonoid.closure x) ≤ x), (fun s x => AddSubmonoid.closure s) x x_1 = (fun s x => AddSubmonoid.closure s) x x_1

Equations

(_ : (fun s x => AddSubmonoid.closure s) x x = (fun s x => AddSubmonoid.closure s) x x) = (_ : (fun s x => AddSubmonoid.closure s) x x = (fun s x => AddSubmonoid.closure s) x x)

def AddSubmonoid.gi (M : Type u_1) [inst : AddZeroClass M] :

GaloisInsertion AddSubmonoid.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

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

def Submonoid.gi (M : Type u_1) [inst : MulOneClass M] :

GaloisInsertion Submonoid.closure SetLike.coe

closure forms a Galois insertion with the coercion to set.

Equations

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

@[simp]

theorem AddSubmonoid.closure_eq {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

AddSubmonoid.closure ↑S = S

Additive closure of an additive submonoid S equals S

@[simp]

theorem Submonoid.closure_eq {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

Submonoid.closure ↑S = S

Closure of a submonoid S equals S.

@[simp]

theorem AddSubmonoid.closure_empty {M : Type u_1} [inst : AddZeroClass M] :

AddSubmonoid.closure ∅ = ⊥

@[simp]

theorem Submonoid.closure_empty {M : Type u_1} [inst : MulOneClass M] :

Submonoid.closure ∅ = ⊥

@[simp]

theorem AddSubmonoid.closure_univ {M : Type u_1} [inst : AddZeroClass M] :

AddSubmonoid.closure Set.univ = ⊤

@[simp]

theorem Submonoid.closure_univ {M : Type u_1} [inst : MulOneClass M] :

Submonoid.closure Set.univ = ⊤

theorem AddSubmonoid.closure_union {M : Type u_1} [inst : AddZeroClass M] (s : Set M) (t : Set M) :

AddSubmonoid.closure (s ∪ t) = AddSubmonoid.closure s ⊔ AddSubmonoid.closure t

theorem Submonoid.closure_union {M : Type u_1} [inst : MulOneClass M] (s : Set M) (t : Set M) :

Submonoid.closure (s ∪ t) = Submonoid.closure s ⊔ Submonoid.closure t

theorem AddSubmonoid.closure_unionᵢ {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} (s : ι → Set M) :

AddSubmonoid.closure (Set.unionᵢ fun i => s i) = ⨆ i, AddSubmonoid.closure (s i)

theorem Submonoid.closure_unionᵢ {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} (s : ι → Set M) :

Submonoid.closure (Set.unionᵢ fun i => s i) = ⨆ i, Submonoid.closure (s i)

theorem AddSubmonoid.closure_singleton_le_iff_mem {M : Type u_1} [inst : AddZeroClass M] (m : M) (p : AddSubmonoid M) :

AddSubmonoid.closure {m} ≤ p ↔ m ∈ p

theorem Submonoid.closure_singleton_le_iff_mem {M : Type u_1} [inst : MulOneClass M] (m : M) (p : Submonoid M) :

Submonoid.closure {m} ≤ p ↔ m ∈ p

theorem AddSubmonoid.mem_supᵢ {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} (p : ι → AddSubmonoid M) {m : M} :

(m ∈ ⨆ i, p i) ↔ ∀ (N : AddSubmonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem Submonoid.mem_supᵢ {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} (p : ι → Submonoid M) {m : M} :

(m ∈ ⨆ i, p i) ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

theorem AddSubmonoid.supᵢ_eq_closure {M : Type u_2} [inst : AddZeroClass M] {ι : Sort u_1} (p : ι → AddSubmonoid M) :

(⨆ i, p i) = AddSubmonoid.closure (Set.unionᵢ fun i => ↑(p i))

theorem Submonoid.supᵢ_eq_closure {M : Type u_2} [inst : MulOneClass M] {ι : Sort u_1} (p : ι → Submonoid M) :

(⨆ i, p i) = Submonoid.closure (Set.unionᵢ fun i => ↑(p i))

theorem AddSubmonoid.disjoint_def {M : Type u_1} [inst : AddZeroClass M] {p₁ : AddSubmonoid M} {p₂ : AddSubmonoid M} :

Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 0

theorem Submonoid.disjoint_def {M : Type u_1} [inst : MulOneClass M] {p₁ : Submonoid M} {p₂ : Submonoid M} :

Disjoint p₁ p₂ ↔ ∀ {x : M}, x ∈ p₁ → x ∈ p₂ → x = 1

theorem AddSubmonoid.disjoint_def' {M : Type u_1} [inst : AddZeroClass M] {p₁ : AddSubmonoid M} {p₂ : AddSubmonoid M} :

Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 0

theorem Submonoid.disjoint_def' {M : Type u_1} [inst : MulOneClass M] {p₁ : Submonoid M} {p₂ : Submonoid M} :

Disjoint p₁ p₂ ↔ ∀ {x y : M}, x ∈ p₁ → y ∈ p₂ → x = y → x = 1

def AddMonoidHom.eqLocusM {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : M →+ N) :

The additive submonoid of elements x : M such that f x = g x

Equations

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

def AddMonoidHom.eqLocusM.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : M →+ N) :

∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a + b) = ↑g (a + b)

Equations

(_ : ↑f (a + b) = ↑g (a + b)) = (_ : ↑f (a + b) = ↑g (a + b))

def AddMonoidHom.eqLocusM.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) (g : M →+ N) :

0 ∈ { carrier := { x | ↑f x = ↑g x }, add_mem' := (_ : ∀ {a b : M}, ↑f a = ↑g a → ↑f b = ↑g b → ↑f (a + b) = ↑g (a + b)) }.carrier

Equations

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

def MonoidHom.eqLocusM {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) (g : M →* N) :

The submonoid of elements x : M such that f x = g x

Equations

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

@[simp]

theorem AddMonoidHom.eqLocusM_same {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M →+ N) :

AddMonoidHom.eqLocusM f f = ⊤

@[simp]

theorem MonoidHom.eqLocusM_same {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M →* N) :

MonoidHom.eqLocusM f f = ⊤

theorem AddMonoidHom.eqOn_closureM {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : M →+ N} {g : M →+ N} {s : Set M} (h : Set.EqOn (↑f) (↑g) s) :

Set.EqOn ↑f ↑g ↑(AddSubmonoid.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem MonoidHom.eqOn_closureM {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {f : M →* N} {g : M →* N} {s : Set M} (h : Set.EqOn (↑f) (↑g) s) :

Set.EqOn ↑f ↑g ↑(Submonoid.closure s)

If two monoid homomorphisms are equal on a set, then they are equal on its submonoid closure.

theorem AddMonoidHom.eq_of_eqOn_topM {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : M →+ N} {g : M →+ N} (h : Set.EqOn ↑f ↑g ↑⊤) :

f = g

theorem MonoidHom.eq_of_eqOn_topM {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {f : M →* N} {g : M →* N} (h : Set.EqOn ↑f ↑g ↑⊤) :

f = g

theorem AddMonoidHom.eq_of_eqOn_denseM {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {s : Set M} (hs : AddSubmonoid.closure s = ⊤) {f : M →+ N} {g : M →+ N} (h : Set.EqOn (↑f) (↑g) s) :

f = g

theorem MonoidHom.eq_of_eqOn_denseM {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {s : Set M} (hs : Submonoid.closure s = ⊤) {f : M →* N} {g : M →* N} (h : Set.EqOn (↑f) (↑g) s) :

f = g

def IsAddUnit.addSubmonoid.proof_2 (M : Type u_1) [inst : AddMonoid M] :

Equations

(_ : IsAddUnit 0) = (_ : IsAddUnit 0)

def IsAddUnit.addSubmonoid (M : Type u_1) [inst : AddMonoid M] :

The additive submonoid consisting of the additive units of an additive monoid

Equations

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

def IsAddUnit.addSubmonoid.proof_1 (M : Type u_1) [inst : AddMonoid M] {a : M} {b : M} (ha : a ∈ setOf IsAddUnit) (hb : b ∈ setOf IsAddUnit) :

a + b ∈ setOf IsAddUnit

Equations

(_ : a + b ∈ setOf IsAddUnit) = (_ : a + b ∈ setOf IsAddUnit)

def IsUnit.submonoid (M : Type u_1) [inst : Monoid M] :

The submonoid consisting of the units of a monoid

Equations

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

theorem IsAddUnit.mem_addSubmonoid_iff {M : Type u_1} [inst : AddMonoid M] (a : M) :

a ∈ IsAddUnit.addSubmonoid M ↔ IsAddUnit a

theorem IsUnit.mem_submonoid_iff {M : Type u_1} [inst : Monoid M] (a : M) :

a ∈ IsUnit.submonoid M ↔ IsUnit a

def AddMonoidHom.ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x + y) = f x + f y) :

M →+ N

Let s be a subset of an additive monoid M such that the closure of s is the whole monoid. Then AddMonoidHom.ofClosureEqTopLeft defines an additive monoid homomorphism from M asking for a proof of f (x + y) = f x + f y only for x ∈ s∈ s.

Equations

AddMonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toZeroHom := { toFun := f, map_zero' := h1 }, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }

def AddMonoidHom.ofClosureMEqTopLeft.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x + y) = f x + f y) (x : M) (y : M) :

f (x + y) = f x + f y

Equations

(_ : ∀ (y : M), f (x + y) = f x + f y) = (_ : ∀ (y : M), f (x + y) = f x + f y)

def MonoidHom.ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] {s : Set M} (f : M → N) (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y) :

M →* N

Let s be a subset of a monoid M such that the closure of s is the whole monoid. Then MonoidHom.ofClosureEqTopLeft defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for x ∈ s∈ s.

Equations

MonoidHom.ofClosureMEqTopLeft f hs h1 hmul = { toOneHom := { toFun := f, map_one' := h1 }, map_mul' := (_ : ∀ (x y : M), f (x * y) = f x * f y) }

@[simp]

theorem AddMonoidHom.coe_ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x + y) = f x + f y) :

↑(AddMonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f

@[simp]

theorem MonoidHom.coe_ofClosureMEqTopLeft {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] {s : Set M} (f : M → N) (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x : M), x ∈ s → ∀ (y : M), f (x * y) = f x * f y) :

↑(MonoidHom.ofClosureMEqTopLeft f hs h1 hmul) = f

def AddMonoidHom.ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) :

M →+ N

Let s be a subset of an additive monoid M such that the closure of s is the whole monoid. Then AddMonoidHom.ofClosureEqTopRight defines an additive monoid homomorphism from M asking for a proof of f (x + y) = f x + f y only for y ∈ s∈ s.

Equations

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

def AddMonoidHom.ofClosureMEqTopRight.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) (x : M) (y : M) :

ZeroHom.toFun { toFun := f, map_zero' := h1 } (x + y) = ZeroHom.toFun { toFun := f, map_zero' := h1 } x + ZeroHom.toFun { toFun := f, map_zero' := h1 } y

Equations

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

def MonoidHom.ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] {s : Set M} (f : M → N) (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) :

M →* N

Let s be a subset of a monoid M such that the closure of s is the whole monoid. Then MonoidHom.ofClosureEqTopRight defines a monoid homomorphism from M asking for a proof of f (x * y) = f x * f y only for y ∈ s∈ s.

Equations

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

@[simp]

theorem AddMonoidHom.coe_ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [inst : AddMonoid M] [inst : AddMonoid N] {s : Set M} (f : M → N) (hs : AddSubmonoid.closure s = ⊤) (h1 : f 0 = 0) (hmul : ∀ (x y : M), y ∈ s → f (x + y) = f x + f y) :

↑(AddMonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f

@[simp]

theorem MonoidHom.coe_ofClosureMEqTopRight {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst : Monoid N] {s : Set M} (f : M → N) (hs : Submonoid.closure s = ⊤) (h1 : f 1 = 1) (hmul : ∀ (x y : M), y ∈ s → f (x * y) = f x * f y) :

↑(MonoidHom.ofClosureMEqTopRight f hs h1 hmul) = f