theorem Submonoid₁.ext {M : Type} : ∀ {inst : Monoid M} {x y : Submonoid₁ M}, x.carrier = y.carrier → x = y

theorem Submonoid₁.ext_iff {M : Type} : ∀ {inst : Monoid M} {x y : Submonoid₁ M}, x = y ↔ x.carrier = y.carrier

structure Submonoid₁ (M : Type) [Monoid M] : Type

• carrier : Set M

  The carrier of a submonoid.

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

  The product of two elements of a submonoid belongs to the submonoid.

• one_mem : 1 ∈ self.carrier

  The unit element belongs to the submonoid.

theorem Submonoid₁.mul_mem {M : Type} [Monoid M] (self : Submonoid₁ M) {a : M} {b : M} : a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier

The product of two elements of a submonoid belongs to the submonoid.

theorem Submonoid₁.one_mem {M : Type} [Monoid M] (self : Submonoid₁ M) : 1 ∈ self.carrier

The unit element belongs to the submonoid.

instance instSetLikeSubmonoid₁ {M : Type} [Monoid M] : SetLike (Submonoid₁ M) M

Submonoids in M can be seen as sets in M.

Equations

• instSetLikeSubmonoid₁ = { coe := Submonoid₁.carrier, coe_injective' := ⋯ }

instance SubMonoid₁Monoid {M : Type} [Monoid M] (N : Submonoid₁ M) : Monoid ↥N

Equations

• SubMonoid₁Monoid N = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

class SubmonoidClass₁ (S : Type) (M : Type) [Monoid M] [SetLike S M] : Prop

• mul_mem : ∀ (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
• one_mem : ∀ (s : S), 1 ∈ s

theorem SubmonoidClass₁.mul_mem {S : Type} {M : Type} : ∀ {inst : Monoid M} {inst_1 : SetLike S M} [self : SubmonoidClass₁ S M] (s : S) {a b : M}, a ∈ s → b ∈ s → a * b ∈ s

theorem SubmonoidClass₁.one_mem {S : Type} {M : Type} : ∀ {inst : Monoid M} {inst_1 : SetLike S M} [self : SubmonoidClass₁ S M] (s : S), 1 ∈ s

instance instSubmonoidClass₁Submonoid₁ {M : Type} [Monoid M] : SubmonoidClass₁ (Submonoid₁ M) M

Equations

• ⋯ = ⋯

instance instInfSubmonoid₁ {M : Type} [Monoid M] : Inf (Submonoid₁ M)

Equations

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

def Submonoid.Setoid {M : Type u_1} [CommMonoid M] (N : Submonoid M) : Setoid M

Equations

• N.Setoid = { r := fun (x y : M) => ∃ w ∈ N, ∃ z ∈ N, x * w = y * z, iseqv := ⋯ }

instance instHasQuotientSubmonoid_leanCourse {M : Type u_1} [CommMonoid M] : HasQuotient M (Submonoid M)

Equations

• instHasQuotientSubmonoid_leanCourse = { quotient' := fun (N : Submonoid M) => Quotient N.Setoid }

def QuotientMonoid.mk {M : Type u_1} [CommMonoid M] (N : Submonoid M) : M → M ⧸ N

Equations

• QuotientMonoid.mk N = Quotient.mk N.Setoid

instance instMonoidQuotientSubmonoid_leanCourse {M : Type u_1} [CommMonoid M] (N : Submonoid M) : Monoid (M ⧸ N)

Equations

• instMonoidQuotientSubmonoid_leanCourse N = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯