Documentation

@[simp]

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

↑(↑(RelIso.toRelEmbedding (RelIso.symm Submonoid.toAddSubmonoid)).toEmbedding S) = ↑Additive.ofMul ⁻¹' ↑S

@[simp]

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

↑(↑(RelIso.toRelEmbedding Submonoid.toAddSubmonoid).toEmbedding S) = ↑Additive.toMul ⁻¹' ↑S

def Submonoid.toAddSubmonoid {M : Type u_1} [inst : MulOneClass M] :

Submonoid M ≃o AddSubmonoid (Additive M)

Submonoids of monoid M are isomorphic to additive submonoids of Additive M.

Equations

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

@[inline]

abbrev AddSubmonoid.toSubmonoid' {M : Type u_1} [inst : MulOneClass M] :

AddSubmonoid (Additive M) ≃o Submonoid M

Additive submonoids of an additive monoid Additive M are isomorphic to submonoids of M.

Equations

AddSubmonoid.toSubmonoid' = OrderIso.symm Submonoid.toAddSubmonoid

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

↑(RelIso.toRelEmbedding Submonoid.toAddSubmonoid).toEmbedding (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)

theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [inst : MulOneClass M] (S : Set (Additive M)) :

↑(RelIso.toRelEmbedding AddSubmonoid.toSubmonoid').toEmbedding (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)

@[simp]

theorem AddSubmonoid.toSubmonoid_apply_coe {A : Type u_1} [inst : AddZeroClass A] (S : AddSubmonoid A) :

↑(↑(RelIso.toRelEmbedding AddSubmonoid.toSubmonoid).toEmbedding S) = ↑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem AddSubmonoid.toSubmonoid_symm_apply_coe {A : Type u_1} [inst : AddZeroClass A] (S : Submonoid (Multiplicative A)) :

↑(↑(RelIso.toRelEmbedding (RelIso.symm AddSubmonoid.toSubmonoid)).toEmbedding S) = ↑Multiplicative.ofAdd ⁻¹' ↑S

def AddSubmonoid.toSubmonoid {A : Type u_1} [inst : AddZeroClass A] :

AddSubmonoid A ≃o Submonoid (Multiplicative A)

Additive submonoids of an additive monoid A are isomorphic to multiplicative submonoids of Multiplicative A.

Equations

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

@[inline]

abbrev Submonoid.toAddSubmonoid' {A : Type u_1} [inst : AddZeroClass A] :

Submonoid (Multiplicative A) ≃o AddSubmonoid A

Submonoids of a monoid Multiplicative A are isomorphic to additive submonoids of A.

Equations

Submonoid.toAddSubmonoid' = OrderIso.symm AddSubmonoid.toSubmonoid

theorem AddSubmonoid.toSubmonoid_closure {A : Type u_1} [inst : AddZeroClass A] (S : Set A) :

↑(RelIso.toRelEmbedding AddSubmonoid.toSubmonoid).toEmbedding (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)

theorem Submonoid.toAddSubmonoid'_closure {A : Type u_1} [inst : AddZeroClass A] (S : Set (Multiplicative A)) :

↑(RelIso.toRelEmbedding Submonoid.toAddSubmonoid').toEmbedding (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)

`comap` and `map` #

def AddSubmonoid.comap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

AddSubmonoid M

The preimage of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations

AddSubmonoid.comap f S = { toAddSubsemigroup := { carrier := ↑f ⁻¹' ↑S, add_mem' := (_ : ∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a + b) ∈ S) }, zero_mem' := (_ : ↑f 0 ∈ S) }

def AddSubmonoid.comap.proof_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

↑f 0 ∈ S

Equations

(_ : ↑f 0 ∈ S) = (_ : ↑f 0 ∈ S)

def AddSubmonoid.comap.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) :

∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a + b) ∈ S

Equations

(_ : ↑f (a + b) ∈ S) = (_ : ↑f (a + b) ∈ S)

def Submonoid.comap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid N) :

Submonoid M

The preimage of a submonoid along a monoid homomorphism is a submonoid.

Equations

Submonoid.comap f S = { toSubsemigroup := { carrier := ↑f ⁻¹' ↑S, mul_mem' := (_ : ∀ {a b : M}, a ∈ ↑f ⁻¹' ↑S → b ∈ ↑f ⁻¹' ↑S → ↑f (a * b) ∈ S) }, one_mem' := (_ : ↑f 1 ∈ S) }

@[simp]

theorem AddSubmonoid.coe_comap {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F) :

↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S

@[simp]

theorem Submonoid.coe_comap {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F) :

↑(Submonoid.comap f S) = ↑f ⁻¹' ↑S

@[simp]

theorem AddSubmonoid.mem_comap {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} {x : M} :

x ∈ AddSubmonoid.comap f S ↔ ↑f x ∈ S

@[simp]

theorem Submonoid.mem_comap {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} {x : M} :

x ∈ Submonoid.comap f S ↔ ↑f x ∈ S

theorem AddSubmonoid.comap_comap {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (S : AddSubmonoid P) (g : N →+ P) (f : M →+ N) :

AddSubmonoid.comap f (AddSubmonoid.comap g S) = AddSubmonoid.comap (AddMonoidHom.comp g f) S

theorem Submonoid.comap_comap {M : Type u_3} {N : Type u_2} {P : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (S : Submonoid P) (g : N →* P) (f : M →* N) :

Submonoid.comap f (Submonoid.comap g S) = Submonoid.comap (MonoidHom.comp g f) S

@[simp]

theorem AddSubmonoid.comap_id {P : Type u_1} [inst : AddZeroClass P] (S : AddSubmonoid P) :

AddSubmonoid.comap (AddMonoidHom.id P) S = S

@[simp]

theorem Submonoid.comap_id {P : Type u_1} [inst : MulOneClass P] (S : Submonoid P) :

Submonoid.comap (MonoidHom.id P) S = S

def AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

∃ a, a ∈ ↑S ∧ ↑f a = 0

Equations

(_ : ∃ a, a ∈ ↑S ∧ ↑f a = 0) = (_ : ∃ a, a ∈ ↑S ∧ ↑f a = 0)

def AddSubmonoid.map.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

∀ {a b : N}, a ∈ ↑f '' ↑S → b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S

Equations

(_ : b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S) = (_ : b ∈ ↑f '' ↑S → a + b ∈ ↑f '' ↑S)

def AddSubmonoid.map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

AddSubmonoid N

The image of an AddSubmonoid along an AddMonoid homomorphism is an AddSubmonoid.

Equations

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

def Submonoid.map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

Submonoid N

The image of a submonoid along a monoid homomorphism is a submonoid.

Equations

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

@[simp]

theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) :

↑(AddSubmonoid.map f S) = ↑f '' ↑S

@[simp]

theorem Submonoid.coe_map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) :

↑(Submonoid.map f S) = ↑f '' ↑S

@[simp]

theorem AddSubmonoid.mem_map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {y : N} :

y ∈ AddSubmonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

@[simp]

theorem Submonoid.mem_map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {y : N} :

y ∈ Submonoid.map f S ↔ ∃ x, x ∈ S ∧ ↑f x = y

theorem AddSubmonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) {S : AddSubmonoid M} {x : M} (hx : x ∈ S) :

↑f x ∈ AddSubmonoid.map f S

theorem Submonoid.mem_map_of_mem {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) {S : Submonoid M} {x : M} (hx : x ∈ S) :

↑f x ∈ Submonoid.map f S

theorem AddSubmonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) (x : { x // x ∈ S }) :

↑f ↑x ∈ AddSubmonoid.map f S

theorem Submonoid.apply_coe_mem_map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) (S : Submonoid M) (x : { x // x ∈ S }) :

↑f ↑x ∈ Submonoid.map f S

theorem AddSubmonoid.map_map {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] [inst : AddZeroClass P] (S : AddSubmonoid M) (g : N →+ P) (f : M →+ N) :

AddSubmonoid.map g (AddSubmonoid.map f S) = AddSubmonoid.map (AddMonoidHom.comp g f) S

theorem Submonoid.map_map {M : Type u_3} {N : Type u_1} {P : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] [inst : MulOneClass P] (S : Submonoid M) (g : N →* P) (f : M →* N) :

Submonoid.map g (Submonoid.map f S) = Submonoid.map (MonoidHom.comp g f) S

theorem AddSubmonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) {S : AddSubmonoid M} {x : M} :

↑f x ∈ AddSubmonoid.map f S ↔ x ∈ S

theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) {S : Submonoid M} {x : M} :

↑f x ∈ Submonoid.map f S ↔ x ∈ S

theorem AddSubmonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} {S : AddSubmonoid M} {T : AddSubmonoid N} :

AddSubmonoid.map f S ≤ T ↔ S ≤ AddSubmonoid.comap f T

theorem Submonoid.map_le_iff_le_comap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} {S : Submonoid M} {T : Submonoid N} :

Submonoid.map f S ≤ T ↔ S ≤ Submonoid.comap f T

theorem AddSubmonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) :

GaloisConnection (AddSubmonoid.map f) (AddSubmonoid.comap f)

theorem Submonoid.gc_map_comap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) :

GaloisConnection (Submonoid.map f) (Submonoid.comap f)

theorem AddSubmonoid.map_le_of_le_comap {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :

S ≤ AddSubmonoid.comap f T → AddSubmonoid.map f S ≤ T

theorem Submonoid.map_le_of_le_comap {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :

S ≤ Submonoid.comap f T → Submonoid.map f S ≤ T

theorem AddSubmonoid.le_comap_of_map_le {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {T : AddSubmonoid N} {f : F} :

AddSubmonoid.map f S ≤ T → S ≤ AddSubmonoid.comap f T

theorem Submonoid.le_comap_of_map_le {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {T : Submonoid N} {f : F} :

Submonoid.map f S ≤ T → S ≤ Submonoid.comap f T

theorem AddSubmonoid.le_comap_map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} :

S ≤ AddSubmonoid.comap f (AddSubmonoid.map f S)

theorem Submonoid.le_comap_map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} :

S ≤ Submonoid.comap f (Submonoid.map f S)

theorem AddSubmonoid.map_comap_le {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} :

AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S

theorem Submonoid.map_comap_le {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :

Submonoid.map f (Submonoid.comap f S) ≤ S

theorem AddSubmonoid.monotone_map {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} :

Monotone (AddSubmonoid.map f)

theorem Submonoid.monotone_map {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} :

Monotone (Submonoid.map f)

theorem AddSubmonoid.monotone_comap {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} :

Monotone (AddSubmonoid.comap f)

theorem Submonoid.monotone_comap {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} :

Monotone (Submonoid.comap f)

@[simp]

theorem AddSubmonoid.map_comap_map {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} :

AddSubmonoid.map f (AddSubmonoid.comap f (AddSubmonoid.map f S)) = AddSubmonoid.map f S

@[simp]

theorem Submonoid.map_comap_map {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} :

Submonoid.map f (Submonoid.comap f (Submonoid.map f S)) = Submonoid.map f S

@[simp]

theorem AddSubmonoid.comap_map_comap {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F} :

AddSubmonoid.comap f (AddSubmonoid.map f (AddSubmonoid.comap f S)) = AddSubmonoid.comap f S

@[simp]

theorem Submonoid.comap_map_comap {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {S : Submonoid N} {f : F} :

Submonoid.comap f (Submonoid.map f (Submonoid.comap f S)) = Submonoid.comap f S

theorem AddSubmonoid.map_sup {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid M) (T : AddSubmonoid M) (f : F) :

AddSubmonoid.map f (S ⊔ T) = AddSubmonoid.map f S ⊔ AddSubmonoid.map f T

theorem Submonoid.map_sup {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S : Submonoid M) (T : Submonoid M) (f : F) :

Submonoid.map f (S ⊔ T) = Submonoid.map f S ⊔ Submonoid.map f T

theorem AddSubmonoid.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid M) :

AddSubmonoid.map f (supᵢ s) = ⨆ i, AddSubmonoid.map f (s i)

theorem Submonoid.map_supᵢ {M : Type u_2} {N : Type u_3} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid M) :

Submonoid.map f (supᵢ s) = ⨆ i, Submonoid.map f (s i)

theorem AddSubmonoid.comap_inf {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (T : AddSubmonoid N) (f : F) :

AddSubmonoid.comap f (S ⊓ T) = AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T

theorem Submonoid.comap_inf {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (S : Submonoid N) (T : Submonoid N) (f : F) :

Submonoid.comap f (S ⊓ T) = Submonoid.comap f S ⊓ Submonoid.comap f T

theorem AddSubmonoid.comap_infᵢ {M : Type u_3} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → AddSubmonoid N) :

AddSubmonoid.comap f (infᵢ s) = ⨅ i, AddSubmonoid.comap f (s i)

theorem Submonoid.comap_infᵢ {M : Type u_3} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_1} (f : F) (s : ι → Submonoid N) :

Submonoid.comap f (infᵢ s) = ⨅ i, Submonoid.comap f (s i)

@[simp]

theorem AddSubmonoid.map_bot {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.map f ⊥ = ⊥

@[simp]

theorem Submonoid.map_bot {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) :

Submonoid.map f ⊥ = ⊥

@[simp]

theorem AddSubmonoid.comap_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) :

AddSubmonoid.comap f ⊤ = ⊤

@[simp]

theorem Submonoid.comap_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] (f : F) :

Submonoid.comap f ⊤ = ⊤

@[simp]

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

AddSubmonoid.map (AddMonoidHom.id M) S = S

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

(x : M) → ∀ (motive : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S → Prop) (x_1 : x ∈ AddSubmonoid.map (AddMonoidHom.id M) S), (∀ (h : x ∈ ↑S), motive (_ : ∃ a, a ∈ ↑S ∧ ↑(AddMonoidHom.id M) a = x)) → motive x_1

Equations

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

@[simp]

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

Submonoid.map (MonoidHom.id M) S = S

def AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : AddSubmonoid M) (x : M) :

x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S

Equations

(_ : x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S) = (_ : x ∈ AddSubmonoid.comap f (AddSubmonoid.map f S) → x ∈ S)

def AddSubmonoid.gciMapComap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

GaloisCoinsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)

map f and comap f form a GaloisCoinsertion when f is injective.

Equations

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

def Submonoid.gciMapComap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

GaloisCoinsertion (Submonoid.map f) (Submonoid.comap f)

map f and comap f form a GaloisCoinsertion when f is injective.

Equations

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

theorem AddSubmonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S) = S

theorem Submonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : Submonoid M) :

Submonoid.comap f (Submonoid.map f S) = S

theorem AddSubmonoid.comap_surjective_of_injective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

Function.Surjective (AddSubmonoid.comap f)

theorem Submonoid.comap_surjective_of_injective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

Function.Surjective (Submonoid.comap f)

theorem AddSubmonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

Function.Injective (AddSubmonoid.map f)

theorem Submonoid.map_injective_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

Function.Injective (Submonoid.map f)

theorem AddSubmonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : AddSubmonoid M) (T : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S ⊓ AddSubmonoid.map f T) = S ⊓ T

theorem Submonoid.comap_inf_map_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : Submonoid M) (T : Submonoid M) :

Submonoid.comap f (Submonoid.map f S ⊓ Submonoid.map f T) = S ⊓ T

theorem AddSubmonoid.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Injective ↑f) (S : ι → AddSubmonoid M) :

AddSubmonoid.comap f (⨅ i, AddSubmonoid.map f (S i)) = infᵢ S

theorem Submonoid.comap_infᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Injective ↑f) (S : ι → Submonoid M) :

Submonoid.comap f (⨅ i, Submonoid.map f (S i)) = infᵢ S

theorem AddSubmonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : AddSubmonoid M) (T : AddSubmonoid M) :

AddSubmonoid.comap f (AddSubmonoid.map f S ⊔ AddSubmonoid.map f T) = S ⊔ T

theorem Submonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) (S : Submonoid M) (T : Submonoid M) :

Submonoid.comap f (Submonoid.map f S ⊔ Submonoid.map f T) = S ⊔ T

theorem AddSubmonoid.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Injective ↑f) (S : ι → AddSubmonoid M) :

AddSubmonoid.comap f (⨆ i, AddSubmonoid.map f (S i)) = supᵢ S

theorem Submonoid.comap_supᵢ_map_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Injective ↑f) (S : ι → Submonoid M) :

Submonoid.comap f (⨆ i, Submonoid.map f (S i)) = supᵢ S

theorem AddSubmonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) {S : AddSubmonoid M} {T : AddSubmonoid M} :

AddSubmonoid.map f S ≤ AddSubmonoid.map f T ↔ S ≤ T

theorem Submonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) {S : Submonoid M} {T : Submonoid M} :

Submonoid.map f S ≤ Submonoid.map f T ↔ S ≤ T

theorem AddSubmonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

StrictMono (AddSubmonoid.map f)

theorem Submonoid.map_strictMono_of_injective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) :

StrictMono (Submonoid.map f)

def AddSubmonoid.giMapComap.proof_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : AddSubmonoid N) (x : N) (h : x ∈ S) :

x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S)

Equations

(_ : x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S)) = (_ : x ∈ AddSubmonoid.map f (AddSubmonoid.comap f S))

def AddSubmonoid.giMapComap {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

GaloisInsertion (AddSubmonoid.map f) (AddSubmonoid.comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Equations

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

abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (x : N) (motive : (∃ a, ↑f a = x) → Prop) :

(x : ∃ a, ↑f a = x) → ((y : M) → (hy : ↑f y = x) → motive (_ : ∃ a, ↑f a = x)) → motive x

Equations

AddSubmonoid.giMapComap.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

def Submonoid.giMapComap {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

GaloisInsertion (Submonoid.map f) (Submonoid.comap f)

map f and comap f form a GaloisInsertion when f is surjective.

Equations

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

theorem AddSubmonoid.map_comap_eq_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S) = S

theorem Submonoid.map_comap_eq_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : Submonoid N) :

Submonoid.map f (Submonoid.comap f S) = S

theorem AddSubmonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

Function.Surjective (AddSubmonoid.map f)

theorem Submonoid.map_surjective_of_surjective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

Function.Surjective (Submonoid.map f)

theorem AddSubmonoid.comap_injective_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

Function.Injective (AddSubmonoid.comap f)

theorem Submonoid.comap_injective_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

Function.Injective (Submonoid.comap f)

theorem AddSubmonoid.map_inf_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : AddSubmonoid N) (T : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S ⊓ AddSubmonoid.comap f T) = S ⊓ T

theorem Submonoid.map_inf_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : Submonoid N) (T : Submonoid N) :

Submonoid.map f (Submonoid.comap f S ⊓ Submonoid.comap f T) = S ⊓ T

theorem AddSubmonoid.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Surjective ↑f) (S : ι → AddSubmonoid N) :

AddSubmonoid.map f (⨅ i, AddSubmonoid.comap f (S i)) = infᵢ S

theorem Submonoid.map_infᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Surjective ↑f) (S : ι → Submonoid N) :

Submonoid.map f (⨅ i, Submonoid.comap f (S i)) = infᵢ S

theorem AddSubmonoid.map_sup_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : AddSubmonoid N) (T : AddSubmonoid N) :

AddSubmonoid.map f (AddSubmonoid.comap f S ⊔ AddSubmonoid.comap f T) = S ⊔ T

theorem Submonoid.map_sup_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) (S : Submonoid N) (T : Submonoid N) :

Submonoid.map f (Submonoid.comap f S ⊔ Submonoid.comap f T) = S ⊔ T

theorem AddSubmonoid.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Surjective ↑f) (S : ι → AddSubmonoid N) :

AddSubmonoid.map f (⨆ i, AddSubmonoid.comap f (S i)) = supᵢ S

theorem Submonoid.map_supᵢ_comap_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {ι : Type u_4} {f : F} (hf : Function.Surjective ↑f) (S : ι → Submonoid N) :

Submonoid.map f (⨆ i, Submonoid.comap f (S i)) = supᵢ S

theorem AddSubmonoid.comap_le_comap_iff_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) {S : AddSubmonoid N} {T : AddSubmonoid N} :

AddSubmonoid.comap f S ≤ AddSubmonoid.comap f T ↔ S ≤ T

theorem Submonoid.comap_le_comap_iff_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) {S : Submonoid N} {T : Submonoid N} :

Submonoid.comap f S ≤ Submonoid.comap f T ↔ S ≤ T

theorem AddSubmonoid.comap_strictMono_of_surjective {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

StrictMono (AddSubmonoid.comap f)

theorem Submonoid.comap_strictMono_of_surjective {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] {F : Type u_3} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) :

StrictMono (Submonoid.comap f)

instance ZeroMemClass.zero {A : Type u_1} {M₁ : Type u_2} [inst : SetLike A M₁] [inst : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :

Zero { x // x ∈ S' }

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

ZeroMemClass.zero S' = { zero := { val := 0, property := (_ : 0 ∈ S') } }

instance OneMemClass.one {A : Type u_1} {M₁ : Type u_2} [inst : SetLike A M₁] [inst : One M₁] [hA : OneMemClass A M₁] (S' : A) :

One { x // x ∈ S' }

A submonoid of a monoid inherits a 1.

Equations

OneMemClass.one S' = { one := { val := 1, property := (_ : 1 ∈ S') } }

@[simp]

theorem ZeroMemClass.coe_zero {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :

↑0 = 0

@[simp]

theorem OneMemClass.coe_one {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : One M₁] [hA : OneMemClass A M₁] (S' : A) :

↑1 = 1

@[simp]

theorem ZeroMemClass.coe_eq_zero {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : Zero M₁] [hA : ZeroMemClass A M₁] {S' : A} {x : { x // x ∈ S' }} :

↑x = 0 ↔ x = 0

@[simp]

theorem OneMemClass.coe_eq_one {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : One M₁] [hA : OneMemClass A M₁] {S' : A} {x : { x // x ∈ S' }} :

↑x = 1 ↔ x = 1

theorem ZeroMemClass.zero_def {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) :

0 = { val := 0, property := (_ : 0 ∈ S') }

theorem OneMemClass.one_def {A : Type u_2} {M₁ : Type u_1} [inst : SetLike A M₁] [inst : One M₁] [hA : OneMemClass A M₁] (S' : A) :

1 = { val := 1, property := (_ : 1 ∈ S') }

instance AddSubmonoidClass.nSMul {M : Type u_1} [inst : AddMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

SMul ℕ { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

Equations

AddSubmonoidClass.nSMul S = { smul := fun n a => { val := n • ↑a, property := (_ : n • ↑a ∈ S) } }

instance SubmonoidClass.nPow {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

Pow { x // x ∈ S } ℕ

A submonoid of a monoid inherits a power operator.

Equations

SubmonoidClass.nPow S = { pow := fun a n => { val := ↑a ^ n, property := (_ : ↑a ^ n ∈ S) } }

@[simp]

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

↑(n • x) = n • ↑x

@[simp]

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

↑(x ^ n) = ↑x ^ n

@[simp]

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

n • { val := x, property := hx } = { val := n • x, property := (_ : n • x ∈ S) }

@[simp]

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

{ val := x, property := hx } ^ n = { val := x ^ n, property := (_ : x ^ n ∈ S) }

instance AddSubmonoidClass.toAddZeroClass {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

AddZeroClass { x // x ∈ S }

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

Equations

AddSubmonoidClass.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))

def AddSubmonoidClass.toAddZeroClass.proof_2 {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoidClass.toAddZeroClass.proof_3 {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoidClass.toAddZeroClass.proof_1 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

instance SubmonoidClass.toMulOneClass {M : Type u_1} [inst : MulOneClass M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

MulOneClass { x // x ∈ S }

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

Equations

SubmonoidClass.toMulOneClass S = Function.Injective.mulOneClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑1 = ↑1) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))

def AddSubmonoidClass.toAddMonoid.proof_5 {M : Type u_1} [inst : AddMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

instance AddSubmonoidClass.toAddMonoid {M : Type u_1} [inst : AddMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

AddMonoid { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

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

def AddSubmonoidClass.toAddMonoid.proof_4 {M : Type u_1} [inst : AddMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoidClass.toAddMonoid.proof_3 {M : Type u_1} [inst : AddMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

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

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

def AddSubmonoidClass.toAddMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

instance SubmonoidClass.toMonoid {M : Type u_1} [inst : Monoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

Monoid { x // x ∈ S }

A submonoid of a monoid inherits a monoid structure.

Equations

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

def AddSubmonoidClass.toAddCommMonoid.proof_4 {M : Type u_1} [inst : AddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoidClass.toAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoidClass.toAddCommMonoid.proof_5 {M : Type u_1} [inst : AddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

instance AddSubmonoidClass.toAddCommMonoid {M : Type u_1} [inst : AddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

AddCommMonoid { x // x ∈ S }

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

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

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

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

def AddSubmonoidClass.toAddCommMonoid.proof_3 {M : Type u_1} [inst : AddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

instance SubmonoidClass.toCommMonoid {M : Type u_1} [inst : CommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

CommMonoid { x // x ∈ S }

A submonoid of a CommMonoid is a CommMonoid.

Equations

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

instance AddSubmonoidClass.toOrderedAddCommMonoid {M : Type u_1} [inst : OrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

OrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

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

def AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [inst : OrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoidClass.toOrderedAddCommMonoid.proof_3 {M : Type u_1} [inst : OrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoidClass.toOrderedAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoidClass.toOrderedAddCommMonoid.proof_1 {M : Type u_2} [inst : OrderedAddCommMonoid M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] :

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

def AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [inst : OrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

instance SubmonoidClass.toOrderedCommMonoid {M : Type u_1} [inst : OrderedCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

OrderedCommMonoid { x // x ∈ S }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

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

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

instance AddSubmonoidClass.toLinearOrderedAddCommMonoid {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

LinearOrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

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

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_2} [inst : LinearOrderedAddCommMonoid M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] :

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

Equations

(_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

def AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

Equations

(_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_1} [inst : LinearOrderedCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

LinearOrderedCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

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

def AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

OrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

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

def AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_2} [inst : OrderedCancelAddCommMonoid M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] :

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_1} [inst : OrderedCancelCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

OrderedCancelCommMonoid { x // x ∈ S }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

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

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

instance AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

LinearOrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

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

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

Equations

(_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} {A : Type u_2} [inst : SetLike A M] (S : A) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] (S : A) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

Equations

(_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_2} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_1} [inst : SetLike A M] [inst : AddSubmonoidClass A M] :

Equations

(_ : ZeroMemClass A M) = (_ : ZeroMemClass A M)

def AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_1} [inst : LinearOrderedCancelCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

LinearOrderedCancelCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

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

def AddSubmonoidClass.Subtype.proof_2 {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] (S' : A) (a : { x // x ∈ S' }) (a : { x // x ∈ S' }) :

↑a + ↑a = ↑a + ↑a

Equations

(_ : ∀ (a a_1 : { x // x ∈ S' }), ↑a + ↑a_1 = ↑a + ↑a_1) = (_ : ∀ (a a_1 : { x // x ∈ S' }), ↑a + ↑a_1 = ↑a + ↑a_1)

def AddSubmonoidClass.Subtype {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :

{ x // x ∈ S' } →+ M

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

Equations

AddSubmonoidClass.Subtype S' = { toZeroHom := { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) }, map_add' := (_ : ∀ (a a_1 : { x // x ∈ S' }), ↑a + ↑a_1 = ↑a + ↑a_1) }

def AddSubmonoidClass.Subtype.proof_1 {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def SubmonoidClass.Subtype {M : Type u_1} [inst : MulOneClass M] {A : Type u_2} [inst : SetLike A M] [hA : SubmonoidClass A M] (S' : A) :

{ x // x ∈ S' } →* M

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

Equations

SubmonoidClass.Subtype S' = { toOneHom := { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) }, map_mul' := (_ : ∀ (a a_1 : { x // x ∈ S' }), ↑a * ↑a_1 = ↑a * ↑a_1) }

@[simp]

theorem AddSubmonoidClass.coe_subtype {M : Type u_1} [inst : AddZeroClass M] {A : Type u_2} [inst : SetLike A M] [hA : AddSubmonoidClass A M] (S' : A) :

↑(AddSubmonoidClass.Subtype S') = Subtype.val

@[simp]

theorem SubmonoidClass.coe_subtype {M : Type u_1} [inst : MulOneClass M] {A : Type u_2} [inst : SetLike A M] [hA : SubmonoidClass A M] (S' : A) :

↑(SubmonoidClass.Subtype S') = Subtype.val

def AddSubmonoid.add.proof_1 {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (a : { x // x ∈ S }) (b : { x // x ∈ S }) :

↑a + ↑b ∈ S

Equations

(_ : ↑a + ↑b ∈ S) = (_ : ↑a + ↑b ∈ S)

instance AddSubmonoid.add {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

Add { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits an addition.

Equations

AddSubmonoid.add S = { add := fun a b => { val := ↑a + ↑b, property := (_ : ↑a + ↑b ∈ S) } }

instance Submonoid.mul {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

Mul { x // x ∈ S }

A submonoid of a monoid inherits a multiplication.

Equations

Submonoid.mul S = { mul := fun a b => { val := ↑a * ↑b, property := (_ : ↑a * ↑b ∈ S) } }

instance AddSubmonoid.zero {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

Zero { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

AddSubmonoid.zero S = { zero := { val := 0, property := (_ : 0 ∈ S) } }

instance Submonoid.one {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

One { x // x ∈ S }

A submonoid of a monoid inherits a 1.

Equations

Submonoid.one S = { one := { val := 1, property := (_ : 1 ∈ S) } }

@[simp]

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

↑(x + y) = ↑x + ↑y

@[simp]

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

↑(x * y) = ↑x * ↑y

@[simp]

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

↑0 = 0

@[simp]

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

↑1 = 1

@[simp]

theorem AddSubmonoid.mk_add_mk {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) :

{ val := x, property := hx } + { val := y, property := hy } = { val := x + y, property := (_ : x + y ∈ S) }

@[simp]

theorem Submonoid.mk_mul_mk {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) (x : M) (y : M) (hx : x ∈ S) (hy : y ∈ S) :

{ val := x, property := hx } * { val := y, property := hy } = { val := x * y, property := (_ : x * y ∈ S) }

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

x + y = { val := ↑x + ↑y, property := (_ : ↑x + ↑y ∈ S) }

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

x * y = { val := ↑x * ↑y, property := (_ : ↑x * ↑y ∈ S) }

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

0 = { val := 0, property := (_ : 0 ∈ S) }

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

1 = { val := 1, property := (_ : 1 ∈ S) }

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

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

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

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

instance AddSubmonoid.toAddZeroClass {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) :

AddZeroClass { x // x ∈ S }

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

Equations

AddSubmonoid.toAddZeroClass S = Function.Injective.addZeroClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑0 = ↑0) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1))

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

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

instance Submonoid.toMulOneClass {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

MulOneClass { x // x ∈ S }

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

Equations

Submonoid.toMulOneClass S = Function.Injective.mulOneClass Subtype.val (_ : Function.Injective fun a => ↑a) (_ : ↑1 = ↑1) (_ : ∀ (x x_1 : { x // x ∈ S }), ↑(x * x_1) = ↑(x * x_1))

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

n • x ∈ S

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

x ^ n ∈ S

def AddSubmonoid.toAddMonoid.proof_2 {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoid.toAddMonoid.proof_3 {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toAddMonoid.proof_4 {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoid.toAddMonoid.proof_1 {M : Type u_1} [inst : AddMonoid M] :

Equations

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

def AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

instance AddSubmonoid.toAddMonoid {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :

AddMonoid { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

Equations

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

instance Submonoid.toMonoid {M : Type u_1} [inst : Monoid M] (S : Submonoid M) :

Monoid { x // x ∈ S }

A submonoid of a monoid inherits a monoid structure.

Equations

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

def AddSubmonoid.toAddCommMonoid.proof_2 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoid.toAddCommMonoid.proof_1 {M : Type u_1} [inst : AddCommMonoid M] :

Equations

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

instance AddSubmonoid.toAddCommMonoid {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :

AddCommMonoid { x // x ∈ S }

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

Equations

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

def AddSubmonoid.toAddCommMonoid.proof_4 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoid.toAddCommMonoid.proof_3 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toAddCommMonoid.proof_5 {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

instance Submonoid.toCommMonoid {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) :

CommMonoid { x // x ∈ S }

A submonoid of a CommMonoid is a CommMonoid.

Equations

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

def AddSubmonoid.toOrderedAddCommMonoid.proof_1 {M : Type u_1} [inst : OrderedAddCommMonoid M] :

Equations

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

instance AddSubmonoid.toOrderedAddCommMonoid {M : Type u_1} [inst : OrderedAddCommMonoid M] (S : AddSubmonoid M) :

OrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

Equations

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

def AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [inst : OrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoid.toOrderedAddCommMonoid.proof_3 {M : Type u_1} [inst : OrderedAddCommMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toOrderedAddCommMonoid.proof_2 {M : Type u_1} [inst : OrderedAddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [inst : OrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

instance Submonoid.toOrderedCommMonoid {M : Type u_1} [inst : OrderedCommMonoid M] (S : Submonoid M) :

OrderedCommMonoid { x // x ∈ S }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

Equations

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

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_2 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

Equations

(_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_3 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] :

Equations

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

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

Equations

(_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

instance AddSubmonoid.toLinearOrderedAddCommMonoid {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :

LinearOrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

Equations

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

instance Submonoid.toLinearOrderedCommMonoid {M : Type u_1} [inst : LinearOrderedCommMonoid M] (S : Submonoid M) :

LinearOrderedCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

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

def AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoid.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] :

Equations

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

def AddSubmonoid.toOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoid.toOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

instance AddSubmonoid.toOrderedCancelAddCommMonoid {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

OrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

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

instance Submonoid.toOrderedCancelCommMonoid {M : Type u_1} [inst : OrderedCancelCommMonoid M] (S : Submonoid M) :

OrderedCancelCommMonoid { x // x ∈ S }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

Equations

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

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_2 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

Function.Injective fun a => ↑a

Equations

(_ : Function.Injective fun a => ↑a) = (_ : Function.Injective fun a => ↑a)

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

Equations

(_ : ↑(x ⊓ x) = ↑(x ⊓ x)) = (_ : ↑(x ⊓ x) = ↑(x ⊓ x))

instance AddSubmonoid.toLinearOrderedCancelAddCommMonoid {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

LinearOrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

Equations

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

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

Equations

(_ : ↑(x • x) = ↑(x • x)) = (_ : ↑(x • x) = ↑(x • x))

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] :

Equations

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

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

Equations

(_ : ↑(x + x) = ↑(x + x)) = (_ : ↑(x + x) = ↑(x + x))

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_3 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :

∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

Equations

(_ : ↑(x ⊔ x) = ↑(x ⊔ x)) = (_ : ↑(x ⊔ x) = ↑(x ⊔ x))

instance Submonoid.toLinearOrderedCancelCommMonoid {M : Type u_1} [inst : LinearOrderedCancelCommMonoid M] (S : Submonoid M) :

LinearOrderedCancelCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

Equations

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

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

{ x // x ∈ S } →+ M

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

Equations

AddSubmonoid.subtype S = { toZeroHom := { toFun := Subtype.val, map_zero' := (_ : ↑0 = ↑0) }, map_add' := (_ : ∀ (a a_1 : { x // x ∈ S }), ↑a + ↑a_1 = ↑a + ↑a_1) }

def AddSubmonoid.subtype.proof_2 {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M) (a : { x // x ∈ S }) (a : { x // x ∈ S }) :

↑a + ↑a = ↑a + ↑a

Equations

(_ : ∀ (a a_1 : { x // x ∈ S }), ↑a + ↑a_1 = ↑a + ↑a_1) = (_ : ∀ (a a_1 : { x // x ∈ S }), ↑a + ↑a_1 = ↑a + ↑a_1)

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

↑0 = ↑0

Equations

(_ : ↑0 = ↑0) = (_ : ↑0 = ↑0)

def Submonoid.subtype {M : Type u_1} [inst : MulOneClass M] (S : Submonoid M) :

{ x // x ∈ S } →* M

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

Equations

Submonoid.subtype S = { toOneHom := { toFun := Subtype.val, map_one' := (_ : ↑1 = ↑1) }, map_mul' := (_ : ∀ (a a_1 : { x // x ∈ S }), ↑a * ↑a_1 = ↑a * ↑a_1) }

@[simp]

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

↑(AddSubmonoid.subtype S) = Subtype.val

@[simp]

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

↑(Submonoid.subtype S) = Subtype.val

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

{ x // x ∈ ⊤ } ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

Equations

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

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

∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)

Equations

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

def AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [inst : AddZeroClass M] (x : { x // x ∈ ⊤ }) :

{ val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x

Equations

(_ : { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x) = (_ : { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x)

def AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [inst : AddZeroClass M] :

∀ (x x_1 : { x // x ∈ ⊤ }), Equiv.toFun { toFun := fun x => ↑x, invFun := fun x => { val := x, property := (_ : x ∈ ⊤) }, left_inv := (_ : ∀ (x : { x // x ∈ ⊤ }), { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x), right_inv := (_ : ∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)) } (x + x_1) = Equiv.toFun { toFun := fun x => ↑x, invFun := fun x => { val := x, property := (_ : x ∈ ⊤) }, left_inv := (_ : ∀ (x : { x // x ∈ ⊤ }), { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x), right_inv := (_ : ∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)) } (x + x_1)

Equations

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

@[simp]

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

↑Submonoid.topEquiv x = ↑x

@[simp]

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

↑AddSubmonoid.topEquiv x = ↑x

@[simp]

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

↑(↑(AddEquiv.symm AddSubmonoid.topEquiv) x) = x

@[simp]

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

↑(↑(MulEquiv.symm Submonoid.topEquiv) x) = x

def Submonoid.topEquiv {M : Type u_1} [inst : MulOneClass M] :

{ x // x ∈ ⊤ } ≃* M

The top submonoid is isomorphic to the monoid.

Equations

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

@[simp]

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

AddEquiv.toAddMonoidHom AddSubmonoid.topEquiv = AddSubmonoid.subtype ⊤

@[simp]

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

MulEquiv.toMonoidHom Submonoid.topEquiv = Submonoid.subtype ⊤

def AddSubmonoid.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ↑f) :

Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun

Equations

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

def AddSubmonoid.equivMapOfInjective.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ↑f) :

∀ (x x_1 : { x // x ∈ S }), Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } x + Equiv.toFun { toFun := (Equiv.Set.image (↑f) (↑S) hf).toFun, invFun := (Equiv.Set.image (↑f) (↑S) hf).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun) } x_1

Equations

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

noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ↑f) :

{ x // x ∈ S } ≃+ { x // x ∈ AddSubmonoid.map f S }

An additive subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use AddEquiv.addSubmonoidMap for better definitional equalities.

Equations

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

def AddSubmonoid.equivMapOfInjective.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ↑f) :

Function.LeftInverse (Equiv.Set.image (↑f) (↑S) hf).invFun (Equiv.Set.image (↑f) (↑S) hf).toFun

Equations

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

noncomputable def Submonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) (f : M →* N) (hf : Function.Injective ↑f) :

{ x // x ∈ S } ≃* { x // x ∈ Submonoid.map f S }

A subgroup is isomorphic to its image under an injective function. If you have an isomorphism, use MulEquiv.submonoidMap for better definitional equalities.

Equations

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

@[simp]

theorem AddSubmonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) (hf : Function.Injective ↑f) (x : { x // x ∈ S }) :

↑(↑(AddSubmonoid.equivMapOfInjective S f hf) x) = ↑f ↑x

@[simp]

theorem Submonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (S : Submonoid M) (f : M →* N) (hf : Function.Injective ↑f) (x : { x // x ∈ S }) :

↑(↑(Submonoid.equivMapOfInjective S f hf) x) = ↑f ↑x

@[simp]

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

AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤

@[simp]

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

Submonoid.closure (Subtype.val ⁻¹' s) = ⊤

def AddSubmonoid.prod {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

AddSubmonoid (M × N)

Given AddSubmonoids s, t of AddMonoids A, B respectively, s × t× t as an AddSubmonoid of A × B× B.

Equations

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

def AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

0.fst ∈ ↑s ∧ 0.snd ∈ ↑t

Equations

(_ : 0.fst ∈ ↑s ∧ 0.snd ∈ ↑t) = (_ : 0.fst ∈ ↑s ∧ 0.snd ∈ ↑t)

def AddSubmonoid.prod.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

∀ {a b : M × N}, a ∈ ↑s ×ˢ ↑t → b ∈ ↑s ×ˢ ↑t → (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t

Equations

(_ : (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t) = (_ : (a + b).fst ∈ ↑s ∧ (a + b).snd ∈ ↑t)

def Submonoid.prod {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) (t : Submonoid N) :

Submonoid (M × N)

Given submonoids s, t of monoids M, N respectively, s × t× t as a submonoid of M × N× N.

Equations

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

theorem AddSubmonoid.coe_prod {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

↑(AddSubmonoid.prod s t) = ↑s ×ˢ ↑t

theorem Submonoid.coe_prod {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) (t : Submonoid N) :

↑(Submonoid.prod s t) = ↑s ×ˢ ↑t

theorem AddSubmonoid.mem_prod {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {p : M × N} :

p ∈ AddSubmonoid.prod s t ↔ p.fst ∈ s ∧ p.snd ∈ t

theorem Submonoid.mem_prod {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {s : Submonoid M} {t : Submonoid N} {p : M × N} :

p ∈ Submonoid.prod s t ↔ p.fst ∈ s ∧ p.snd ∈ t

theorem AddSubmonoid.prod_mono {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {s₁ : AddSubmonoid M} {s₂ : AddSubmonoid M} {t₁ : AddSubmonoid N} {t₂ : AddSubmonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

AddSubmonoid.prod s₁ t₁ ≤ AddSubmonoid.prod s₂ t₂

theorem Submonoid.prod_mono {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {s₁ : Submonoid M} {s₂ : Submonoid M} {t₁ : Submonoid N} {t₂ : Submonoid N} (hs : s₁ ≤ s₂) (ht : t₁ ≤ t₂) :

Submonoid.prod s₁ t₁ ≤ Submonoid.prod s₂ t₂

theorem AddSubmonoid.prod_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) :

AddSubmonoid.prod s ⊤ = AddSubmonoid.comap (AddMonoidHom.fst M N) s

theorem Submonoid.prod_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) :

Submonoid.prod s ⊤ = Submonoid.comap (MonoidHom.fst M N) s

theorem AddSubmonoid.top_prod {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid N) :

AddSubmonoid.prod ⊤ s = AddSubmonoid.comap (AddMonoidHom.snd M N) s

theorem Submonoid.top_prod {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid N) :

Submonoid.prod ⊤ s = Submonoid.comap (MonoidHom.snd M N) s

@[simp]

theorem AddSubmonoid.top_prod_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddSubmonoid.prod ⊤ ⊤ = ⊤

@[simp]

theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Submonoid.prod ⊤ ⊤ = ⊤

theorem AddSubmonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :

AddSubmonoid.prod ⊥ ⊥ = ⊥

theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :

Submonoid.prod ⊥ ⊥ = ⊥

def AddSubmonoid.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

Equations

(_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)

def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

{ x // x ∈ AddSubmonoid.prod s t } ≃+ { x // x ∈ s } × { x // x ∈ t }

The product of additive submonoids is isomorphic to their product as additive monoids

Equations

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

def AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

Equations

(_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) = (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun)

def AddSubmonoid.prodEquiv.proof_3 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

∀ (x x_1 : { x // x ∈ AddSubmonoid.prod s t }), Equiv.toFun { toFun := (Equiv.Set.prod ↑s ↑t).toFun, invFun := (Equiv.Set.prod ↑s ↑t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) } (x + x_1) = Equiv.toFun { toFun := (Equiv.Set.prod ↑s ↑t).toFun, invFun := (Equiv.Set.prod ↑s ↑t).invFun, left_inv := (_ : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun), right_inv := (_ : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun) } (x + x_1)

Equations

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

def Submonoid.prodEquiv {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) (t : Submonoid N) :

{ x // x ∈ Submonoid.prod s t } ≃* { x // x ∈ s } × { x // x ∈ t }

The product of submonoids is isomorphic to their product as monoids.

Equations

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

abbrev AddSubmonoid.map_inl.match_1 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p ∈ AddSubmonoid.map (AddMonoidHom.inl M N) s → Prop) :

(x : p ∈ AddSubmonoid.map (AddMonoidHom.inl M N) s) → ((w : M) → (hx : w ∈ ↑s) → (hp : ↑(AddMonoidHom.inl M N) w = p) → motive (_ : ∃ a, a ∈ ↑s ∧ ↑(AddMonoidHom.inl M N) a = p)) → motive x

Equations

AddSubmonoid.map_inl.match_1 s p motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

abbrev AddSubmonoid.map_inl.match_2 {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (p : M × N) (motive : p ∈ AddSubmonoid.prod s ⊥ → Prop) :

(x : p ∈ AddSubmonoid.prod s ⊥) → ((hps : p.fst ∈ ↑s) → (hp1 : p.snd ∈ ↑⊥) → motive (_ : p.fst ∈ ↑s ∧ p.snd ∈ ↑⊥)) → motive x

Equations

AddSubmonoid.map_inl.match_2 s p motive x h_1 = And.casesOn x fun left right => h_1 left right

theorem AddSubmonoid.map_inl {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) :

AddSubmonoid.map (AddMonoidHom.inl M N) s = AddSubmonoid.prod s ⊥

theorem Submonoid.map_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) :

Submonoid.map (MonoidHom.inl M N) s = Submonoid.prod s ⊥

abbrev AddSubmonoid.map_inr.match_2 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p ∈ AddSubmonoid.prod ⊥ s → Prop) :

(x : p ∈ AddSubmonoid.prod ⊥ s) → ((hp1 : p.fst ∈ ↑⊥) → (hps : p.snd ∈ ↑s) → motive (_ : p.fst ∈ ↑⊥ ∧ p.snd ∈ ↑s)) → motive x

Equations

AddSubmonoid.map_inr.match_2 s p motive x h_1 = And.casesOn x fun left right => h_1 left right

abbrev AddSubmonoid.map_inr.match_1 {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid N) (p : M × N) (motive : p ∈ AddSubmonoid.map (AddMonoidHom.inr M N) s → Prop) :

(x : p ∈ AddSubmonoid.map (AddMonoidHom.inr M N) s) → ((w : N) → (hx : w ∈ ↑s) → (hp : ↑(AddMonoidHom.inr M N) w = p) → motive (_ : ∃ a, a ∈ ↑s ∧ ↑(AddMonoidHom.inr M N) a = p)) → motive x

Equations

AddSubmonoid.map_inr.match_1 s p motive x h_1 = Exists.casesOn x fun w h => And.casesOn h fun left right => h_1 w left right

theorem AddSubmonoid.map_inr {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid N) :

AddSubmonoid.map (AddMonoidHom.inr M N) s = AddSubmonoid.prod ⊥ s

theorem Submonoid.map_inr {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid N) :

Submonoid.map (MonoidHom.inr M N) s = Submonoid.prod ⊥ s

@[simp]

theorem AddSubmonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) :

AddSubmonoid.prod s ⊥ ⊔ AddSubmonoid.prod ⊥ t = AddSubmonoid.prod s t

@[simp]

theorem Submonoid.prod_bot_sup_bot_prod {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) (t : Submonoid N) :

Submonoid.prod s ⊥ ⊔ Submonoid.prod ⊥ t = Submonoid.prod s t

theorem AddSubmonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {f : M ≃+ N} {K : AddSubmonoid M} {x : N} :

x ∈ AddSubmonoid.map (AddEquiv.toAddMonoidHom f) K ↔ ↑(AddEquiv.symm f) x ∈ K

theorem Submonoid.mem_map_equiv {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {f : M ≃* N} {K : Submonoid M} {x : N} :

x ∈ Submonoid.map (MulEquiv.toMonoidHom f) K ↔ ↑(MulEquiv.symm f) x ∈ K

theorem AddSubmonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M ≃+ N) (K : AddSubmonoid M) :

AddSubmonoid.map (AddEquiv.toAddMonoidHom f) K = AddSubmonoid.comap (AddEquiv.toAddMonoidHom (AddEquiv.symm f)) K

theorem Submonoid.map_equiv_eq_comap_symm {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M ≃* N) (K : Submonoid M) :

Submonoid.map (MulEquiv.toMonoidHom f) K = Submonoid.comap (MulEquiv.toMonoidHom (MulEquiv.symm f)) K

theorem AddSubmonoid.comap_equiv_eq_map_symm {M : Type u_2} {N : Type u_1} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : N ≃+ M) (K : AddSubmonoid M) :

AddSubmonoid.comap (AddEquiv.toAddMonoidHom f) K = AddSubmonoid.map (AddEquiv.toAddMonoidHom (AddEquiv.symm f)) K

theorem Submonoid.comap_equiv_eq_map_symm {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (f : N ≃* M) (K : Submonoid M) :

Submonoid.comap (MulEquiv.toMonoidHom f) K = Submonoid.map (MulEquiv.toMonoidHom (MulEquiv.symm f)) K

@[simp]

theorem AddSubmonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M ≃+ N) :

AddSubmonoid.map (AddEquiv.toAddMonoidHom f) ⊤ = ⊤

@[simp]

theorem Submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M ≃* N) :

Submonoid.map (MulEquiv.toMonoidHom f) ⊤ = ⊤

theorem AddSubmonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} :

u ≤ AddSubmonoid.prod s t ↔ AddSubmonoid.map (AddMonoidHom.fst M N) u ≤ s ∧ AddSubmonoid.map (AddMonoidHom.snd M N) u ≤ t