Submonoids: definition

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.
• MonoidHom.eqLocusM: the submonoid of elements x : M such that f x = g x;

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_3) (M : outParam (Type u_4)) [One M] [SetLike S M] : Prop

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

• one_mem : ∀ (s : S), 1 ∈ s

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

theorem OneMemClass.one_mem {S : Type u_3} {M : outParam (Type u_4)} : ∀ {inst : One M} {inst_1 : SetLike S M} [self : OneMemClass S M] (s : S), 1 ∈ s

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

class ZeroMemClass (S : Type u_3) (M : outParam (Type u_4)) [Zero M] [SetLike S M] : Prop

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

• zero_mem : ∀ (s : S), 0 ∈ s

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

theorem ZeroMemClass.zero_mem {S : Type u_3} {M : outParam (Type u_4)} : ∀ {inst : Zero M} {inst_1 : SetLike S M} [self : ZeroMemClass S M] (s : S), 0 ∈ s

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

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

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

• carrier : Set M
• mul_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
• one_mem' : 1 ∈ self.carrier

  A submonoid contains 1.

theorem Submonoid.one_mem' {M : Type u_3} [MulOneClass M] (self : Submonoid M) : 1 ∈ self.carrier

A submonoid contains 1.

class SubmonoidClass (S : Type u_3) (M : outParam (Type u_4)) [MulOneClass M] [SetLike S M] extends MulMemClass , OneMemClass : Prop

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

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

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

• carrier : Set M
• add_mem' : ∀ {a b : M}, a ∈ self.carrier → b ∈ self.carrier → a + b ∈ self.carrier
• zero_mem' : 0 ∈ self.carrier

  An additive submonoid contains 0.

theorem AddSubmonoid.zero_mem' {M : Type u_3} [AddZeroClass M] (self : AddSubmonoid M) : 0 ∈ self.carrier

An additive submonoid contains 0.

class AddSubmonoidClass (S : Type u_3) (M : outParam (Type u_4)) [AddZeroClass M] [SetLike S M] extends AddMemClass , ZeroMemClass : Prop

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

theorem nsmul_mem {M : Type u_3} {A : Type u_4} [AddMonoid M] [SetLike A M] [AddSubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) : n • x ∈ S

theorem pow_mem {M : Type u_3} {A : Type u_4} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S

instance AddSubmonoid.instSetLike {M : Type u_1} [AddZeroClass M] : SetLike (AddSubmonoid M) M

Equations

• AddSubmonoid.instSetLike = { coe := fun (s : AddSubmonoid M) => s.carrier, coe_injective' := ⋯ }

theorem AddSubmonoid.instSetLike.proof_1 {M : Type u_1} [AddZeroClass M] (p : AddSubmonoid M) (q : AddSubmonoid M) (h : (fun (s : AddSubmonoid M) => s.carrier) p = (fun (s : AddSubmonoid M) => s.carrier) q) : p = q

instance Submonoid.instSetLike {M : Type u_1} [MulOneClass M] : SetLike (Submonoid M) M

Equations

• Submonoid.instSetLike = { coe := fun (s : Submonoid M) => s.carrier, coe_injective' := ⋯ }

instance AddSubmonoid.instAddSubmonoidClass {M : Type u_1} [AddZeroClass M] : AddSubmonoidClass (AddSubmonoid M) M

Equations

• ⋯ = ⋯

instance Submonoid.instSubmonoidClass {M : Type u_1} [MulOneClass M] : SubmonoidClass (Submonoid M) M

Equations

• ⋯ = ⋯

@[simp]

theorem AddSubmonoid.mem_toSubsemigroup {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} : x ∈ s.toAddSubsemigroup ↔ x ∈ s

@[simp]

theorem Submonoid.mem_toSubsemigroup {M : Type u_1} [MulOneClass M] {s : Submonoid M} {x : M} : x ∈ s.toSubsemigroup ↔ x ∈ s

theorem AddSubmonoid.mem_carrier {M : Type u_1} [AddZeroClass M] {s : AddSubmonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s

theorem Submonoid.mem_carrier {M : Type u_1} [MulOneClass M] {s : Submonoid M} {x : M} : x ∈ s.carrier ↔ x ∈ s

@[simp]

theorem AddSubmonoid.mem_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} {x : M} (h_one : 0 ∈ s.carrier) : x ∈ { toAddSubsemigroup := s, zero_mem' := h_one } ↔ x ∈ s

@[simp]

theorem Submonoid.mem_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} {x : M} (h_one : 1 ∈ s.carrier) : x ∈ { toSubsemigroup := s, one_mem' := h_one } ↔ x ∈ s

@[simp]

theorem AddSubmonoid.coe_set_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} (h_one : 0 ∈ s.carrier) : ↑{ toAddSubsemigroup := s, zero_mem' := h_one } = ↑s

@[simp]

theorem Submonoid.coe_set_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} (h_one : 1 ∈ s.carrier) : ↑{ toSubsemigroup := s, one_mem' := h_one } = ↑s

@[simp]

theorem AddSubmonoid.mk_le_mk {M : Type u_1} [AddZeroClass M] {s : AddSubsemigroup M} {t : AddSubsemigroup M} (h_one : 0 ∈ s.carrier) (h_one' : 0 ∈ t.carrier) : { toAddSubsemigroup := s, zero_mem' := h_one } ≤ { toAddSubsemigroup := t, zero_mem' := h_one' } ↔ s ≤ t

@[simp]

theorem Submonoid.mk_le_mk {M : Type u_1} [MulOneClass M] {s : Subsemigroup M} {t : Subsemigroup M} (h_one : 1 ∈ s.carrier) (h_one' : 1 ∈ t.carrier) : { toSubsemigroup := s, one_mem' := h_one } ≤ { toSubsemigroup := t, one_mem' := h_one' } ↔ s ≤ t

theorem AddSubmonoid.ext {M : Type u_1} [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 AddSubmonoid.ext_iff {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} : S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T

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

theorem Submonoid.ext {M : Type u_1} [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.

theorem AddSubmonoid.copy.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (s : Set M) (hs : s = ↑S) : ∀ {a b : M}, a ∈ s → b ∈ s → a + b ∈ s

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

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

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

Equations

• S.copy s hs = { carrier := s, add_mem' := ⋯, zero_mem' := ⋯ }

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

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

Equations

• S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

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

@[simp]

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

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

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

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

An AddSubmonoid contains the monoid's 0.

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

A submonoid contains the monoid's 1.

theorem AddSubmonoid.add_mem {M : Type u_1} [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} [MulOneClass M] (S : Submonoid M) {x : M} {y : M} : x ∈ S → y ∈ S → x * y ∈ S

A submonoid is closed under multiplication.

theorem AddSubmonoid.instTop.proof_2 {M : Type u_1} [AddZeroClass M] : 0 ∈ Set.univ

theorem AddSubmonoid.instTop.proof_1 {M : Type u_1} [AddZeroClass M] : ∀ {a b : M}, a ∈ Set.univ → b ∈ Set.univ → a + b ∈ Set.univ

instance AddSubmonoid.instTop {M : Type u_1} [AddZeroClass M] : Top (AddSubmonoid M)

The additive submonoid M of the AddMonoid M.

Equations

• AddSubmonoid.instTop = { top := { carrier := Set.univ, add_mem' := ⋯, zero_mem' := ⋯ } }

instance Submonoid.instTop {M : Type u_1} [MulOneClass M] : Top (Submonoid M)

The submonoid M of the monoid M.

Equations

• Submonoid.instTop = { top := { carrier := Set.univ, mul_mem' := ⋯, one_mem' := ⋯ } }

theorem AddSubmonoid.instBot.proof_2 {M : Type u_1} [AddZeroClass M] : 0 ∈ {0}

theorem AddSubmonoid.instBot.proof_1 {M : Type u_1} [AddZeroClass M] : ∀ {a b : M}, a ∈ {0} → b ∈ {0} → a + b ∈ {0}

instance AddSubmonoid.instBot {M : Type u_1} [AddZeroClass M] : Bot (AddSubmonoid M)

The trivial AddSubmonoid {0} of an AddMonoid M.

Equations

• AddSubmonoid.instBot = { bot := { carrier := {0}, add_mem' := ⋯, zero_mem' := ⋯ } }

instance Submonoid.instBot {M : Type u_1} [MulOneClass M] : Bot (Submonoid M)

The trivial submonoid {1} of a monoid M.

Equations

• Submonoid.instBot = { bot := { carrier := {1}, mul_mem' := ⋯, one_mem' := ⋯ } }

instance AddSubmonoid.instInhabited {M : Type u_1} [AddZeroClass M] : Inhabited (AddSubmonoid M)

Equations

• AddSubmonoid.instInhabited = { default := ⊥ }

instance Submonoid.instInhabited {M : Type u_1} [MulOneClass M] : Inhabited (Submonoid M)

Equations

• Submonoid.instInhabited = { default := ⊥ }

@[simp]

theorem AddSubmonoid.mem_bot {M : Type u_1} [AddZeroClass M] {x : M} : x ∈ ⊥ ↔ x = 0

@[simp]

theorem Submonoid.mem_bot {M : Type u_1} [MulOneClass M] {x : M} : x ∈ ⊥ ↔ x = 1

@[simp]

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

@[simp]

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

@[simp]

theorem AddSubmonoid.coe_top {M : Type u_1} [AddZeroClass M] : ↑⊤ = Set.univ

@[simp]

theorem Submonoid.coe_top {M : Type u_1} [MulOneClass M] : ↑⊤ = Set.univ

@[simp]

theorem AddSubmonoid.coe_bot {M : Type u_1} [AddZeroClass M] : ↑⊥ = {0}

@[simp]

theorem Submonoid.coe_bot {M : Type u_1} [MulOneClass M] : ↑⊥ = {1}

theorem AddSubmonoid.instInf.proof_1 {M : Type u_1} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) : ∀ {a b : M}, a ∈ ↑S₁ ∩ ↑S₂ → b ∈ ↑S₁ ∩ ↑S₂ → a + b ∈ ↑S₁ ∩ ↑S₂

instance AddSubmonoid.instInf {M : Type u_1} [AddZeroClass M] : Inf (AddSubmonoid M)

The inf of two AddSubmonoids is their intersection.

Equations

• AddSubmonoid.instInf = { inf := fun (S₁ S₂ : AddSubmonoid M) => { carrier := ↑S₁ ∩ ↑S₂, add_mem' := ⋯, zero_mem' := ⋯ } }

theorem AddSubmonoid.instInf.proof_2 {M : Type u_1} [AddZeroClass M] (S₁ : AddSubmonoid M) (S₂ : AddSubmonoid M) : 0 ∈ ↑S₁ ∧ 0 ∈ ↑S₂

instance Submonoid.instInf {M : Type u_1} [MulOneClass M] : Inf (Submonoid M)

The inf of two submonoids is their intersection.

Equations

• Submonoid.instInf = { inf := fun (S₁ S₂ : Submonoid M) => { carrier := ↑S₁ ∩ ↑S₂, mul_mem' := ⋯, one_mem' := ⋯ } }

@[simp]

theorem AddSubmonoid.coe_inf {M : Type u_1} [AddZeroClass M] (p : AddSubmonoid M) (p' : AddSubmonoid M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem Submonoid.coe_inf {M : Type u_1} [MulOneClass M] (p : Submonoid M) (p' : Submonoid M) : ↑(p ⊓ p') = ↑p ∩ ↑p'

@[simp]

theorem AddSubmonoid.mem_inf {M : Type u_1} [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} [MulOneClass M] {p : Submonoid M} {p' : Submonoid M} {x : M} : x ∈ p ⊓ p' ↔ x ∈ p ∧ x ∈ p'

@[simp]

theorem AddSubmonoid.subsingleton_iff {M : Type u_1} [AddZeroClass M] : Subsingleton (AddSubmonoid M) ↔ Subsingleton M

@[simp]

theorem Submonoid.subsingleton_iff {M : Type u_1} [MulOneClass M] : Subsingleton (Submonoid M) ↔ Subsingleton M

@[simp]

theorem AddSubmonoid.nontrivial_iff {M : Type u_1} [AddZeroClass M] : Nontrivial (AddSubmonoid M) ↔ Nontrivial M

@[simp]

theorem Submonoid.nontrivial_iff {M : Type u_1} [MulOneClass M] : Nontrivial (Submonoid M) ↔ Nontrivial M

theorem AddSubmonoid.instUniqueOfSubsingleton.proof_1 {M : Type u_1} [AddZeroClass M] [Subsingleton M] (a : AddSubmonoid M) : a = default

instance AddSubmonoid.instUniqueOfSubsingleton {M : Type u_1} [AddZeroClass M] [Subsingleton M] : Unique (AddSubmonoid M)

Equations

• AddSubmonoid.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance Submonoid.instUniqueOfSubsingleton {M : Type u_1} [MulOneClass M] [Subsingleton M] : Unique (Submonoid M)

Equations

• Submonoid.instUniqueOfSubsingleton = { default := ⊥, uniq := ⋯ }

instance AddSubmonoid.instNontrivial {M : Type u_1} [AddZeroClass M] [Nontrivial M] : Nontrivial (AddSubmonoid M)

Equations

• ⋯ = ⋯

instance Submonoid.instNontrivial {M : Type u_1} [MulOneClass M] [Nontrivial M] : Nontrivial (Submonoid M)

Equations

• ⋯ = ⋯

theorem AddMonoidHom.eqLocusM.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [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)

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

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

Equations

• f.eqLocusM g = { carrier := {x : M | f x = g x}, add_mem' := ⋯, zero_mem' := ⋯ }

theorem AddMonoidHom.eqLocusM.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (g : M →+ N) : 0 ∈ { carrier := {x : M | f x = g x}, add_mem' := ⋯ }.carrier

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

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

Equations

• f.eqLocusM g = { carrier := {x : M | f x = g x}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

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

@[simp]

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

theorem AddMonoidHom.eq_of_eqOn_topM {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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} [MulOneClass M] [MulOneClass N] {f : M →* N} {g : M →* N} (h : Set.EqOn ⇑f ⇑g ↑⊤) : f = g

instance ZeroMemClass.zero {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : Zero ↥S'

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

• ZeroMemClass.zero S' = { zero := ⟨0, ⋯⟩ }

instance OneMemClass.one {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : One ↥S'

A submonoid of a monoid inherits a 1.

Equations

• OneMemClass.one S' = { one := ⟨1, ⋯⟩ }

@[simp]

theorem ZeroMemClass.coe_zero {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : ↑0 = 0

@[simp]

theorem OneMemClass.coe_one {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : ↑1 = 1

@[simp]

theorem ZeroMemClass.coe_eq_zero {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : ↥S'} : ↑x = 0 ↔ x = 0

@[simp]

theorem OneMemClass.coe_eq_one {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] {S' : A} {x : ↥S'} : ↑x = 1 ↔ x = 1

theorem ZeroMemClass.zero_def {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : 0 = ⟨0, ⋯⟩

theorem OneMemClass.one_def {A : Type u_3} {M₁ : Type u_4} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : 1 = ⟨1, ⋯⟩

instance AddSubmonoidClass.nSMul {M : Type u_5} [AddMonoid M] {A : Type u_4} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ ↥S

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

Equations

• AddSubmonoidClass.nSMul S = { smul := fun (n : ℕ) (a : ↥S) => ⟨n • ↑a, ⋯⟩ }

instance SubmonoidClass.nPow {M : Type u_5} [Monoid M] {A : Type u_4} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow ↥S ℕ

A submonoid of a monoid inherits a power operator.

Equations

• SubmonoidClass.nPow S = { pow := fun (a : ↥S) (n : ℕ) => ⟨↑a ^ n, ⋯⟩ }

@[simp]

theorem AddSubmonoidClass.coe_nsmul {M : Type u_5} [AddMonoid M] {A : Type u_4} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : ↥S) (n : ℕ) : ↑(n • x) = n • ↑x

@[simp]

theorem SubmonoidClass.coe_pow {M : Type u_5} [Monoid M] {A : Type u_4} [SetLike A M] [SubmonoidClass A M] {S : A} (x : ↥S) (n : ℕ) : ↑(x ^ n) = ↑x ^ n

@[simp]

theorem AddSubmonoidClass.mk_nsmul {M : Type u_5} [AddMonoid M] {A : Type u_4} [SetLike A M] [AddSubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : n • ⟨x, hx⟩ = ⟨n • x, ⋯⟩

@[simp]

theorem SubmonoidClass.mk_pow {M : Type u_5} [Monoid M] {A : Type u_4} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : ⟨x, hx⟩ ^ n = ⟨x ^ n, ⋯⟩

theorem AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

@[instance 75]

instance AddSubmonoidClass.toAddZeroClass {M : Type u_4} [AddZeroClass M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddZeroClass ↥S

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations

• AddSubmonoidClass.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [AddZeroClass M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

@[instance 75]

instance SubmonoidClass.toMulOneClass {M : Type u_4} [MulOneClass M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : MulOneClass ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

• SubmonoidClass.toMulOneClass S = Function.Injective.mulOneClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

@[instance 75]

instance AddSubmonoidClass.toAddMonoid {M : Type u_4} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddMonoid ↥S

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

• AddSubmonoidClass.toAddMonoid S = Function.Injective.addMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

theorem AddSubmonoidClass.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoidClass.toAddMonoid.proof_1 {M : Type u_2} [AddMonoid M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

@[instance 75]

instance SubmonoidClass.toMonoid {M : Type u_4} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : Monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

• SubmonoidClass.toMonoid S = Function.Injective.monoid Subtype.val ⋯ ⋯ ⋯ ⋯

@[instance 75]

instance AddSubmonoidClass.toAddCommMonoid {M : Type u_5} [AddCommMonoid M] {A : Type u_4} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddCommMonoid ↥S

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

• AddSubmonoidClass.toAddCommMonoid S = Function.Injective.addCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoidClass.toAddCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ↑0 = ↑0

theorem AddSubmonoidClass.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toAddCommMonoid.proof_1 {M : Type u_2} [AddCommMonoid M] {A : Type u_1} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

theorem AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [SetLike A M] (S : A) : Function.Injective fun (a : ↥S) => ↑a

@[instance 75]

instance SubmonoidClass.toCommMonoid {M : Type u_5} [CommMonoid M] {A : Type u_4} [SetLike A M] [SubmonoidClass A M] (S : A) : CommMonoid ↥S

A submonoid of a CommMonoid is a CommMonoid.

Equations

• SubmonoidClass.toCommMonoid S = Function.Injective.commMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

def AddSubmonoidClass.subtype {M : Type u_1} {A : Type u_3} [AddZeroClass M] [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ↥S' →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations

• AddSubmonoidClass.subtype S' = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

theorem AddSubmonoidClass.subtype.proof_1 {M : Type u_1} {A : Type u_2} [AddZeroClass M] [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ↑0 = ↑0

theorem AddSubmonoidClass.subtype.proof_2 {M : Type u_1} {A : Type u_2} [AddZeroClass M] [SetLike A M] (S' : A) : ∀ (x x_1 : ↥S'), ↑x + ↑x_1 = ↑x + ↑x_1

def SubmonoidClass.subtype {M : Type u_1} {A : Type u_3} [MulOneClass M] [SetLike A M] [hA : SubmonoidClass A M] (S' : A) : ↥S' →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

• SubmonoidClass.subtype S' = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubmonoidClass.coe_subtype {M : Type u_1} {A : Type u_3} [AddZeroClass M] [SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) : ⇑(AddSubmonoidClass.subtype S') = Subtype.val

@[simp]

theorem SubmonoidClass.coe_subtype {M : Type u_1} {A : Type u_3} [MulOneClass M] [SetLike A M] [hA : SubmonoidClass A M] (S' : A) : ⇑(SubmonoidClass.subtype S') = Subtype.val

theorem AddSubmonoid.add.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) (a : ↥S) (b : ↥S) : ↑a + ↑b ∈ S

instance AddSubmonoid.add {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : Add ↥S

An AddSubmonoid of an AddMonoid inherits an addition.

Equations

• S.add = { add := fun (a b : ↥S) => ⟨↑a + ↑b, ⋯⟩ }

instance Submonoid.mul {M : Type u_4} [MulOneClass M] (S : Submonoid M) : Mul ↥S

A submonoid of a monoid inherits a multiplication.

Equations

• S.mul = { mul := fun (a b : ↥S) => ⟨↑a * ↑b, ⋯⟩ }

instance AddSubmonoid.zero {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : Zero ↥S

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

• S.zero = { zero := ⟨0, ⋯⟩ }

instance Submonoid.one {M : Type u_4} [MulOneClass M] (S : Submonoid M) : One ↥S

A submonoid of a monoid inherits a 1.

Equations

• S.one = { one := ⟨1, ⋯⟩ }

@[simp]

theorem AddSubmonoid.coe_add {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) (x : ↥S) (y : ↥S) : ↑(x + y) = ↑x + ↑y

@[simp]

theorem Submonoid.coe_mul {M : Type u_4} [MulOneClass M] (S : Submonoid M) (x : ↥S) (y : ↥S) : ↑(x * y) = ↑x * ↑y

@[simp]

theorem AddSubmonoid.coe_zero {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = 0

@[simp]

theorem Submonoid.coe_one {M : Type u_4} [MulOneClass M] (S : Submonoid M) : ↑1 = 1

@[simp]

theorem AddSubmonoid.mk_eq_zero {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) {a : M} {ha : a ∈ S} : ⟨a, ha⟩ = 0 ↔ a = 0

@[simp]

theorem Submonoid.mk_eq_one {M : Type u_4} [MulOneClass M] (S : Submonoid M) {a : M} {ha : a ∈ S} : ⟨a, ha⟩ = 1 ↔ a = 1

@[simp]

theorem AddSubmonoid.mk_add_mk {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) : ⟨x, hx⟩ + ⟨y, hy⟩ = ⟨x + y, ⋯⟩

@[simp]

theorem Submonoid.mk_mul_mk {M : Type u_4} [MulOneClass M] (S : Submonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) : ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩

theorem AddSubmonoid.add_def {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) (x : ↥S) (y : ↥S) : x + y = ⟨↑x + ↑y, ⋯⟩

theorem Submonoid.mul_def {M : Type u_4} [MulOneClass M] (S : Submonoid M) (x : ↥S) (y : ↥S) : x * y = ⟨↑x * ↑y, ⋯⟩

theorem AddSubmonoid.zero_def {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : 0 = ⟨0, ⋯⟩

theorem Submonoid.one_def {M : Type u_4} [MulOneClass M] (S : Submonoid M) : 1 = ⟨1, ⋯⟩

theorem AddSubmonoid.toAddZeroClass.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = ↑0

instance AddSubmonoid.toAddZeroClass {M : Type u_5} [AddZeroClass M] (S : AddSubmonoid M) : AddZeroClass ↥S

An AddSubmonoid of a unital additive magma inherits a unital additive magma structure.

Equations

• S.toAddZeroClass = Function.Injective.addZeroClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddZeroClass.proof_3 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toAddZeroClass.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

instance Submonoid.toMulOneClass {M : Type u_5} [MulOneClass M] (S : Submonoid M) : MulOneClass ↥S

A submonoid of a unital magma inherits a unital magma structure.

Equations

• S.toMulOneClass = Function.Injective.mulOneClass Subtype.val ⋯ ⋯ ⋯

theorem AddSubmonoid.nsmul_mem {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : n • x ∈ S

theorem Submonoid.pow_mem {M : Type u_5} [Monoid M] (S : Submonoid M) {x : M} (hx : x ∈ S) (n : ℕ) : x ^ n ∈ S

instance AddSubmonoid.toAddMonoid {M : Type u_5} [AddMonoid M] (S : AddSubmonoid M) : AddMonoid ↥S

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

• S.toAddMonoid = Function.Injective.addMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toAddMonoid.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

theorem AddSubmonoid.toAddMonoid.proof_3 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.toAddMonoid.proof_1 {M : Type u_1} [AddMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

instance Submonoid.toMonoid {M : Type u_5} [Monoid M] (S : Submonoid M) : Monoid ↥S

A submonoid of a monoid inherits a monoid structure.

Equations

• S.toMonoid = Function.Injective.monoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : ↥S) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toAddCommMonoid.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toAddCommMonoid.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : Function.Injective fun (a : ↥S) => ↑a

instance AddSubmonoid.toAddCommMonoid {M : Type u_5} [AddCommMonoid M] (S : AddSubmonoid M) : AddCommMonoid ↥S

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

• S.toAddCommMonoid = Function.Injective.addCommMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

theorem AddSubmonoid.toAddCommMonoid.proof_1 {M : Type u_1} [AddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toAddCommMonoid.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ↑0 = ↑0

instance Submonoid.toCommMonoid {M : Type u_5} [CommMonoid M] (S : Submonoid M) : CommMonoid ↥S

A submonoid of a CommMonoid is a CommMonoid.

Equations

• S.toCommMonoid = Function.Injective.commMonoid Subtype.val ⋯ ⋯ ⋯ ⋯

def AddSubmonoid.subtype {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : ↥S →+ M

The natural monoid hom from an AddSubmonoid of AddMonoid M to M.

Equations

• S.subtype = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }

theorem AddSubmonoid.subtype.proof_1 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = ↑0

theorem AddSubmonoid.subtype.proof_2 {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : ∀ (x x_1 : ↥S), ↑x + ↑x_1 = ↑x + ↑x_1

def Submonoid.subtype {M : Type u_4} [MulOneClass M] (S : Submonoid M) : ↥S →* M

The natural monoid hom from a submonoid of monoid M to M.

Equations

• S.subtype = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem AddSubmonoid.coe_subtype {M : Type u_4} [AddZeroClass M] (S : AddSubmonoid M) : ⇑S.subtype = Subtype.val

@[simp]

theorem Submonoid.coe_subtype {M : Type u_4} [MulOneClass M] (S : Submonoid M) : ⇑S.subtype = Subtype.val