Operations on Submonoids

In this file we define various operations on Submonoids and MonoidHoms.

Main definitions

Conversion between multiplicative and additive definitions

• Submonoid.toAddSubmonoid, Submonoid.toAddSubmonoid', AddSubmonoid.toSubmonoid, AddSubmonoid.toSubmonoid': convert between multiplicative and additive submonoids of M, Multiplicative M, and Additive M. These are stated as OrderIsos.

(Commutative) monoid structure on a submonoid

• Submonoid.toMonoid, Submonoid.toCommMonoid: a submonoid inherits a (commutative) monoid structure.

Group actions by submonoids

• Submonoid.MulAction, Submonoid.DistribMulAction: a submonoid inherits (distributive) multiplicative actions.

Operations on submonoids

• Submonoid.comap: preimage of a submonoid under a monoid homomorphism as a submonoid of the domain;
• Submonoid.map: image of a submonoid under a monoid homomorphism as a submonoid of the codomain;
• Submonoid.prod: product of two submonoids s : Submonoid M and t : Submonoid N as a submonoid of M × N;

Monoid homomorphisms between submonoid

• Submonoid.subtype: embedding of a submonoid into the ambient monoid.
• Submonoid.inclusion: given two submonoids S, T such that S ≤ T, S.inclusion T is the inclusion of S into T as a monoid homomorphism;
• MulEquiv.submonoidCongr: converts a proof of S = T into a monoid isomorphism between S and T.
• Submonoid.prodEquiv: monoid isomorphism between s.prod t and s × t;

Operations on MonoidHoms

• MonoidHom.mrange: range of a monoid homomorphism as a submonoid of the codomain;
• MonoidHom.mker: kernel of a monoid homomorphism as a submonoid of the domain;
• MonoidHom.restrict: restrict a monoid homomorphism to a submonoid;
• MonoidHom.codRestrict: restrict the codomain of a monoid homomorphism to a submonoid;
• MonoidHom.mrangeRestrict: restrict a monoid homomorphism to its range;

Tags

submonoid, range, product, map, comap

Conversion to/from Additive/Multiplicative

@[simp]

theorem Submonoid.toAddSubmonoid_apply_coe {M : Type u_1} [MulOneClass M] (S : Submonoid M) : ↑(↑Submonoid.toAddSubmonoid S) = ↑Additive.toMul ⁻¹' ↑S

@[simp]

theorem Submonoid.toAddSubmonoid_symm_apply_coe {M : Type u_1} [MulOneClass M] (S : AddSubmonoid (Additive M)) : ↑(↑(RelIso.symm Submonoid.toAddSubmonoid) S) = ↑Additive.ofMul ⁻¹' ↑S

def Submonoid.toAddSubmonoid {M : Type u_1} [MulOneClass M] : Submonoid M ≃o AddSubmonoid (Additive M)

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

@[inline, reducible]

abbrev AddSubmonoid.toSubmonoid' {M : Type u_1} [MulOneClass M] : AddSubmonoid (Additive M) ≃o Submonoid M

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

theorem Submonoid.toAddSubmonoid_closure {M : Type u_1} [MulOneClass M] (S : Set M) : ↑Submonoid.toAddSubmonoid (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.toMul ⁻¹' S)

theorem AddSubmonoid.toSubmonoid'_closure {M : Type u_1} [MulOneClass M] (S : Set (Additive M)) : ↑AddSubmonoid.toSubmonoid' (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.ofAdd ⁻¹' S)

@[simp]

theorem AddSubmonoid.toSubmonoid_apply_coe {A : Type u_4} [AddZeroClass A] (S : AddSubmonoid A) : ↑(↑AddSubmonoid.toSubmonoid S) = ↑Multiplicative.toAdd ⁻¹' ↑S

@[simp]

theorem AddSubmonoid.toSubmonoid_symm_apply_coe {A : Type u_4} [AddZeroClass A] (S : Submonoid (Multiplicative A)) : ↑(↑(RelIso.symm AddSubmonoid.toSubmonoid) S) = ↑Multiplicative.ofAdd ⁻¹' ↑S

def AddSubmonoid.toSubmonoid {A : Type u_4} [AddZeroClass A] : AddSubmonoid A ≃o Submonoid (Multiplicative A)

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

@[inline, reducible]

abbrev Submonoid.toAddSubmonoid' {A : Type u_4} [AddZeroClass A] : Submonoid (Multiplicative A) ≃o AddSubmonoid A

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

theorem AddSubmonoid.toSubmonoid_closure {A : Type u_4} [AddZeroClass A] (S : Set A) : ↑AddSubmonoid.toSubmonoid (AddSubmonoid.closure S) = Submonoid.closure (↑Multiplicative.toAdd ⁻¹' S)

theorem Submonoid.toAddSubmonoid'_closure {A : Type u_4} [AddZeroClass A] (S : Set (Multiplicative A)) : ↑Submonoid.toAddSubmonoid' (Submonoid.closure S) = AddSubmonoid.closure (↑Additive.ofMul ⁻¹' S)

comap and map

theorem AddSubmonoid.comap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid N) : ↑f 0 ∈ S

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

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

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

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

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

@[simp]

theorem AddSubmonoid.coe_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (S : AddSubmonoid N) (f : F) : ↑(AddSubmonoid.comap f S) = ↑f ⁻¹' ↑S

@[simp]

theorem Submonoid.coe_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (S : Submonoid N) (f : F) : ↑(Submonoid.comap f S) = ↑f ⁻¹' ↑S

@[simp]

theorem AddSubmonoid.mem_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [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_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [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_3} [AddZeroClass P] (S : AddSubmonoid P) : AddSubmonoid.comap (AddMonoidHom.id P) S = S

@[simp]

theorem Submonoid.comap_id {P : Type u_3} [MulOneClass P] (S : Submonoid P) : Submonoid.comap (MonoidHom.id P) S = S

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

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

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

theorem AddSubmonoid.map.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M) : ∃ a, a ∈ ↑S ∧ ↑f a = 0

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

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

@[simp]

theorem AddSubmonoid.coe_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [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_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [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

@[simp]

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

@[simp]

theorem Submonoid.mem_map_iff_mem {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) : GaloisConnection (Submonoid.map f) (Submonoid.comap f)

theorem AddSubmonoid.map_le_of_le_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} : S ≤ Submonoid.comap f (Submonoid.map f S)

theorem AddSubmonoid.map_comap_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} : Monotone (AddSubmonoid.map f)

theorem Submonoid.monotone_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} : Monotone (Submonoid.map f)

theorem AddSubmonoid.monotone_comap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} : Monotone (AddSubmonoid.comap f)

theorem Submonoid.monotone_comap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} : Monotone (Submonoid.comap f)

@[simp]

theorem AddSubmonoid.map_comap_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iSup {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid M) : AddSubmonoid.map f (iSup s) = ⨆ (i : ι), AddSubmonoid.map f (s i)

theorem Submonoid.map_iSup {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid M) : Submonoid.map f (iSup s) = ⨆ (i : ι), Submonoid.map f (s i)

theorem AddSubmonoid.comap_inf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iInf {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → AddSubmonoid N) : AddSubmonoid.comap f (iInf s) = ⨅ (i : ι), AddSubmonoid.comap f (s i)

theorem Submonoid.comap_iInf {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Sort u_5} (f : F) (s : ι → Submonoid N) : Submonoid.comap f (iInf s) = ⨅ (i : ι), Submonoid.comap f (s i)

@[simp]

theorem AddSubmonoid.map_bot {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid.map f ⊥ = ⊥

@[simp]

theorem Submonoid.map_bot {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) : Submonoid.map f ⊥ = ⊥

@[simp]

theorem AddSubmonoid.comap_top {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid.comap f ⊤ = ⊤

@[simp]

theorem Submonoid.comap_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] (f : F) : Submonoid.comap f ⊤ = ⊤

@[simp]

theorem AddSubmonoid.map_id {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : AddSubmonoid.map (AddMonoidHom.id M) S = S

abbrev AddSubmonoid.map_id.match_1 {M : Type u_1} [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

@[simp]

theorem Submonoid.map_id {M : Type u_1} [MulOneClass M] (S : Submonoid M) : Submonoid.map (MonoidHom.id M) S = S

theorem AddSubmonoid.gciMapComap.proof_1 {M : Type u_1} {N : Type u_3} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [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

def AddSubmonoid.gciMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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.

def Submonoid.gciMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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.

theorem AddSubmonoid.comap_map_eq_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ↑f) (S : ι → AddSubmonoid M) : AddSubmonoid.comap f (⨅ (i : ι), AddSubmonoid.map f (S i)) = iInf S

theorem Submonoid.comap_iInf_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ↑f) (S : ι → Submonoid M) : Submonoid.comap f (⨅ (i : ι), Submonoid.map f (S i)) = iInf S

theorem AddSubmonoid.comap_sup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ↑f) (S : ι → AddSubmonoid M) : AddSubmonoid.comap f (⨆ (i : ι), AddSubmonoid.map f (S i)) = iSup S

theorem Submonoid.comap_iSup_map_of_injective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Injective ↑f) (S : ι → Submonoid M) : Submonoid.comap f (⨆ (i : ι), Submonoid.map f (S i)) = iSup S

theorem AddSubmonoid.map_le_map_iff_of_injective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {f : F} (hf : Function.Injective ↑f) : StrictMono (Submonoid.map f)

def AddSubmonoid.giMapComap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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.

abbrev AddSubmonoid.giMapComap.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

theorem AddSubmonoid.giMapComap.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_2} [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)

def Submonoid.giMapComap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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.

theorem AddSubmonoid.map_comap_eq_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ↑f) (S : ι → AddSubmonoid N) : AddSubmonoid.map f (⨅ (i : ι), AddSubmonoid.comap f (S i)) = iInf S

theorem Submonoid.map_iInf_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ↑f) (S : ι → Submonoid N) : Submonoid.map f (⨅ (i : ι), Submonoid.comap f (S i)) = iInf S

theorem AddSubmonoid.map_sup_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ↑f) (S : ι → AddSubmonoid N) : AddSubmonoid.map f (⨆ (i : ι), AddSubmonoid.comap f (S i)) = iSup S

theorem Submonoid.map_iSup_comap_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F} (hf : Function.Surjective ↑f) (S : ι → Submonoid N) : Submonoid.map f (⨆ (i : ι), Submonoid.comap f (S i)) = iSup S

theorem AddSubmonoid.comap_le_comap_iff_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [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_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_4} [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_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_4} [mc : AddMonoidHomClass F M N] {f : F} (hf : Function.Surjective ↑f) : StrictMono (AddSubmonoid.comap f)

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

instance ZeroMemClass.zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : Zero { x // x ∈ S' }

An AddSubmonoid of an AddMonoid inherits a zero.

instance OneMemClass.one {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : One { x // x ∈ S' }

A submonoid of a monoid inherits a 1.

@[simp]

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

@[simp]

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

@[simp]

theorem ZeroMemClass.coe_eq_zero {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [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_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] {S' : A} {x : { x // x ∈ S' }} : ↑x = 1 ↔ x = 1

theorem ZeroMemClass.zero_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [Zero M₁] [hA : ZeroMemClass A M₁] (S' : A) : 0 = { val := 0, property := (_ : 0 ∈ S') }

theorem OneMemClass.one_def {A : Type u_4} {M₁ : Type u_5} [SetLike A M₁] [One M₁] [hA : OneMemClass A M₁] (S' : A) : 1 = { val := 1, property := (_ : 1 ∈ S') }

instance AddSubmonoidClass.nSMul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : SMul ℕ { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits a scalar multiplication.

instance SubmonoidClass.nPow {M : Type u_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : Pow { x // x ∈ S } ℕ

A submonoid of a monoid inherits a power operator.

@[simp]

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

@[simp]

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

@[simp]

theorem AddSubmonoidClass.mk_nsmul {M : Type u_6} [AddMonoid M] {A : Type u_5} [SetLike A M] [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_6} [Monoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] {S : A} (x : M) (hx : x ∈ S) (n : ℕ) : { val := x, property := hx } ^ n = { val := x ^ n, property := (_ : x ^ n ∈ S) }

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

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 AddSubmonoidClass.toAddZeroClass {M : Type u_5} [AddZeroClass M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddZeroClass { x // x ∈ S }

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

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 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance SubmonoidClass.toMulOneClass {M : Type u_5} [MulOneClass M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) : MulOneClass { x // x ∈ S }

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

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_1 {M : Type u_1} [AddMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

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

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 : { x // x ∈ 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 => ↑a

instance AddSubmonoidClass.toAddMonoid {M : Type u_5} [AddMonoid M] {A : Type u_6} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddMonoid { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

instance SubmonoidClass.toMonoid {M : Type u_5} [Monoid M] {A : Type u_6} [SetLike A M] [SubmonoidClass A M] (S : A) : Monoid { x // x ∈ S }

A submonoid of a monoid inherits a monoid structure.

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_1 {M : Type u_1} [AddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] : ZeroMemClass A M

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 : { x // x ∈ 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 : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance AddSubmonoidClass.toAddCommMonoid {M : Type u_6} [AddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : AddCommMonoid { x // x ∈ S }

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

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

instance SubmonoidClass.toCommMonoid {M : Type u_6} [CommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : CommMonoid { x // x ∈ S }

A submonoid of a CommMonoid is a CommMonoid.

instance AddSubmonoidClass.toOrderedAddCommMonoid {M : Type u_6} [OrderedAddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : OrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

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

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

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

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance SubmonoidClass.toOrderedCommMonoid {M : Type u_6} [OrderedCommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : OrderedCommMonoid { x // x ∈ S }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

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

instance AddSubmonoidClass.toLinearOrderedAddCommMonoid {M : Type u_6} [LinearOrderedAddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : LinearOrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

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

theorem AddSubmonoidClass.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

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

instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_6} [LinearOrderedCommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : LinearOrderedCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

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

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_6} [OrderedCancelAddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : OrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

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

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

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_6} [OrderedCancelCommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : OrderedCancelCommMonoid { x // x ∈ S }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid {M : Type u_6} [LinearOrderedCancelAddCommMonoid M] {A : Type u_5} [SetLike A M] [AddSubmonoidClass A M] (S : A) : LinearOrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

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

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] (S : A) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

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

theorem AddSubmonoidClass.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass A M] (S : A) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_6} [LinearOrderedCancelCommMonoid M] {A : Type u_5} [SetLike A M] [SubmonoidClass A M] (S : A) : LinearOrderedCancelCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

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

def AddSubmonoidClass.subtype {M : Type u_1} [AddZeroClass M] {A : Type u_4} [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.

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

def SubmonoidClass.subtype {M : Type u_1} [MulOneClass M] {A : Type u_4} [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.

@[simp]

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

@[simp]

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

instance AddSubmonoid.add {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Add { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits an addition.

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

instance Submonoid.mul {M : Type u_1} [MulOneClass M] (S : Submonoid M) : Mul { x // x ∈ S }

A submonoid of a monoid inherits a multiplication.

instance AddSubmonoid.zero {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : Zero { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits a zero.

instance Submonoid.one {M : Type u_1} [MulOneClass M] (S : Submonoid M) : One { x // x ∈ S }

A submonoid of a monoid inherits a 1.

@[simp]

theorem AddSubmonoid.coe_add {M : Type u_1} [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} [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} [AddZeroClass M] (S : AddSubmonoid M) : ↑0 = 0

@[simp]

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

@[simp]

theorem AddSubmonoid.mk_add_mk {M : Type u_1} [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} [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} [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} [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} [AddZeroClass M] (S : AddSubmonoid M) : 0 = { val := 0, property := (_ : 0 ∈ S) }

theorem Submonoid.one_def {M : Type u_1} [MulOneClass M] (S : Submonoid M) : 1 = { val := 1, property := (_ : 1 ∈ S) }

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

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

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

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

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

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

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

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

theorem AddSubmonoid.toAddMonoid.proof_5 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∀ (x : { x // 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 => ↑a

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

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

An AddSubmonoid of an AddMonoid inherits an AddMonoid structure.

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

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

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

A submonoid of a monoid inherits a monoid structure.

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

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

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

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

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

An AddSubmonoid of an AddCommMonoid is an AddCommMonoid.

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

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

A submonoid of a CommMonoid is a CommMonoid.

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

instance AddSubmonoid.toOrderedAddCommMonoid {M : Type u_5} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : OrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedAddCommMonoid is an OrderedAddCommMonoid.

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_5 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_1 {M : Type u_1} [OrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toOrderedAddCommMonoid.proof_4 {M : Type u_1} [OrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance Submonoid.toOrderedCommMonoid {M : Type u_5} [OrderedCommMonoid M] (S : Submonoid M) : OrderedCommMonoid { x // x ∈ S }

A submonoid of an OrderedCommMonoid is an OrderedCommMonoid.

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

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

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

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toLinearOrderedAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

instance AddSubmonoid.toLinearOrderedAddCommMonoid {M : Type u_5} [LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

instance Submonoid.toLinearOrderedCommMonoid {M : Type u_5} [LinearOrderedCommMonoid M] (S : Submonoid M) : LinearOrderedCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

instance AddSubmonoid.toOrderedCancelAddCommMonoid {M : Type u_5} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : OrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

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

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [OrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

theorem AddSubmonoid.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [OrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

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

instance Submonoid.toOrderedCancelCommMonoid {M : Type u_5} [OrderedCancelCommMonoid M] (S : Submonoid M) : OrderedCancelCommMonoid { x // x ∈ S }

A submonoid of an OrderedCancelCommMonoid is an OrderedCancelCommMonoid.

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] : AddSubmonoidClass (AddSubmonoid M) M

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_7 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊓ x_1) = ↑(x ⊓ x_1)

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

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_4 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x + x_1) = ↑(x + x_1)

instance AddSubmonoid.toLinearOrderedCancelAddCommMonoid {M : Type u_5} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : LinearOrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of a LinearOrderedCancelAddCommMonoid is a LinearOrderedCancelAddCommMonoid.

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_5 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x : { x // x ∈ S }) (x_1 : ℕ), ↑(x_1 • x) = ↑(x_1 • x)

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

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_6 {M : Type u_1} [LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) : ∀ (x x_1 : { x // x ∈ S }), ↑(x ⊔ x_1) = ↑(x ⊔ x_1)

instance Submonoid.toLinearOrderedCancelCommMonoid {M : Type u_5} [LinearOrderedCancelCommMonoid M] (S : Submonoid M) : LinearOrderedCancelCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCancelCommMonoid is a LinearOrderedCancelCommMonoid.

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

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

def AddSubmonoid.subtype {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) : { x // x ∈ S } →+ M

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

def Submonoid.subtype {M : Type u_1} [MulOneClass M] (S : Submonoid M) : { x // x ∈ S } →* M

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

@[simp]

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

@[simp]

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

theorem AddSubmonoid.topEquiv.proof_1 {M : Type u_1} [AddZeroClass M] (x : { x // x ∈ ⊤ }) : { val := ↑x, property := (_ : (fun x => ↑x) x ∈ ⊤) } = x

theorem AddSubmonoid.topEquiv.proof_3 {M : Type u_1} [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)

theorem AddSubmonoid.topEquiv.proof_2 {M : Type u_1} [AddZeroClass M] : ∀ (x : M), (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x) = (fun x => ↑x) ((fun x => { val := x, property := (_ : x ∈ ⊤) }) x)

def AddSubmonoid.topEquiv {M : Type u_1} [AddZeroClass M] : { x // x ∈ ⊤ } ≃+ M

The top additive submonoid is isomorphic to the additive monoid.

@[simp]

theorem AddSubmonoid.topEquiv_symm_apply_coe {M : Type u_1} [AddZeroClass M] (x : M) : ↑(↑(AddEquiv.symm AddSubmonoid.topEquiv) x) = x

@[simp]

theorem Submonoid.topEquiv_symm_apply_coe {M : Type u_1} [MulOneClass M] (x : M) : ↑(↑(MulEquiv.symm Submonoid.topEquiv) x) = x

@[simp]

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

@[simp]

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

def Submonoid.topEquiv {M : Type u_1} [MulOneClass M] : { x // x ∈ ⊤ } ≃* M

The top submonoid is isomorphic to the monoid.

@[simp]

theorem AddSubmonoid.topEquiv_toAddMonoidHom {M : Type u_1} [AddZeroClass M] : AddEquiv.toAddMonoidHom AddSubmonoid.topEquiv = AddSubmonoid.subtype ⊤

@[simp]

theorem Submonoid.topEquiv_toMonoidHom {M : Type u_1} [MulOneClass M] : MulEquiv.toMonoidHom Submonoid.topEquiv = Submonoid.subtype ⊤

noncomputable def AddSubmonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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.

theorem AddSubmonoid.equivMapOfInjective.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

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

theorem AddSubmonoid.equivMapOfInjective.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

noncomputable def Submonoid.equivMapOfInjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [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.

@[simp]

theorem AddSubmonoid.coe_equivMapOfInjective_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] {s : Set M} : AddSubmonoid.closure (Subtype.val ⁻¹' s) = ⊤

@[simp]

theorem Submonoid.closure_closure_coe_preimage {M : Type u_1} [MulOneClass M] {s : Set M} : Submonoid.closure (Subtype.val ⁻¹' s) = ⊤

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

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

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

theorem AddSubmonoid.prod.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : 0.fst ∈ ↑s ∧ 0.snd ∈ ↑t

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

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

theorem AddSubmonoid.coe_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [MulOneClass N] (s : Submonoid M) : Submonoid.prod s ⊤ = Submonoid.comap (MonoidHom.fst M N) s

theorem AddSubmonoid.top_prod {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) : AddSubmonoid.prod ⊤ s = AddSubmonoid.comap (AddMonoidHom.snd M N) s

theorem Submonoid.top_prod {M : Type u_1} {N : Type u_2} [MulOneClass M] [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} [AddZeroClass M] [AddZeroClass N] : AddSubmonoid.prod ⊤ ⊤ = ⊤

@[simp]

theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : Submonoid.prod ⊤ ⊤ = ⊤

theorem AddSubmonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddSubmonoid.prod ⊥ ⊥ = ⊥

theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : Submonoid.prod ⊥ ⊥ = ⊥

theorem AddSubmonoid.prodEquiv.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : Function.LeftInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

def AddSubmonoid.prodEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

theorem AddSubmonoid.prodEquiv.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid M) (t : AddSubmonoid N) : Function.RightInverse (Equiv.Set.prod ↑s ↑t).invFun (Equiv.Set.prod ↑s ↑t).toFun

theorem AddSubmonoid.prodEquiv.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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)

def Submonoid.prodEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [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.

abbrev AddSubmonoid.map_inl.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

abbrev AddSubmonoid.map_inl.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

theorem AddSubmonoid.map_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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} [MulOneClass M] [MulOneClass N] (s : Submonoid M) : Submonoid.map (MonoidHom.inl M N) s = Submonoid.prod s ⊥

theorem AddSubmonoid.map_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (s : AddSubmonoid N) : AddSubmonoid.map (AddMonoidHom.inr M N) s = AddSubmonoid.prod ⊥ s

abbrev AddSubmonoid.map_inr.match_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

abbrev AddSubmonoid.map_inr.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

theorem Submonoid.map_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [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} [AddZeroClass M] [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} [MulOneClass M] [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_1} {N : Type u_2} [AddZeroClass M] [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_1} {N : Type u_2} [MulOneClass M] [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} [AddZeroClass M] [AddZeroClass N] (f : M ≃+ N) : AddSubmonoid.map (AddEquiv.toAddMonoidHom f) ⊤ = ⊤

@[simp]

theorem Submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M ≃* N) : Submonoid.map (MulEquiv.toMonoidHom f) ⊤ = ⊤

theorem AddSubmonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [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

theorem Submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : u ≤ Submonoid.prod s t ↔ Submonoid.map (MonoidHom.fst M N) u ≤ s ∧ Submonoid.map (MonoidHom.snd M N) u ≤ t

theorem AddSubmonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {s : AddSubmonoid M} {t : AddSubmonoid N} {u : AddSubmonoid (M × N)} : AddSubmonoid.prod s t ≤ u ↔ AddSubmonoid.map (AddMonoidHom.inl M N) s ≤ u ∧ AddSubmonoid.map (AddMonoidHom.inr M N) t ≤ u

theorem Submonoid.prod_le_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} {u : Submonoid (M × N)} : Submonoid.prod s t ≤ u ↔ Submonoid.map (MonoidHom.inl M N) s ≤ u ∧ Submonoid.map (MonoidHom.inr M N) t ≤ u

theorem AddMonoidHom.mrange.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {F : Type u_3} [mc : AddMonoidHomClass F M N] (f : F) : Set.range ↑f = ↑f '' Set.univ

def AddMonoidHom.mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid N

The range of an AddMonoidHom is an AddSubmonoid.

def MonoidHom.mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : Submonoid N

The range of a monoid homomorphism is a submonoid. See Note [range copy pattern].

@[simp]

theorem AddMonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : ↑(AddMonoidHom.mrange f) = Set.range ↑f

@[simp]

theorem MonoidHom.coe_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : ↑(MonoidHom.mrange f) = Set.range ↑f

@[simp]

theorem AddMonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] {f : F} {y : N} : y ∈ AddMonoidHom.mrange f ↔ ∃ x, ↑f x = y

@[simp]

theorem MonoidHom.mem_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] {f : F} {y : N} : y ∈ MonoidHom.mrange f ↔ ∃ x, ↑f x = y

theorem AddMonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : AddMonoidHom.mrange f = AddSubmonoid.map f ⊤

theorem MonoidHom.mrange_eq_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : MonoidHom.mrange f = Submonoid.map f ⊤

theorem AddMonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) : AddSubmonoid.map g (AddMonoidHom.mrange f) = AddMonoidHom.mrange (AddMonoidHom.comp g f)

theorem MonoidHom.map_mrange {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) : Submonoid.map g (MonoidHom.mrange f) = MonoidHom.mrange (MonoidHom.comp g f)

theorem AddMonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] {f : F} : AddMonoidHom.mrange f = ⊤ ↔ Function.Surjective ↑f

theorem MonoidHom.mrange_top_iff_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] {f : F} : MonoidHom.mrange f = ⊤ ↔ Function.Surjective ↑f

@[simp]

theorem AddMonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) (hf : Function.Surjective ↑f) : AddMonoidHom.mrange f = ⊤

The range of a surjective AddMonoid hom is the whole of the codomain.

@[simp]

theorem MonoidHom.mrange_top_of_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (hf : Function.Surjective ↑f) : MonoidHom.mrange f = ⊤

The range of a surjective monoid hom is the whole of the codomain.

theorem AddMonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) (s : Set N) : AddSubmonoid.closure (↑f ⁻¹' s) ≤ AddSubmonoid.comap f (AddSubmonoid.closure s)

theorem MonoidHom.mclosure_preimage_le {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (s : Set N) : Submonoid.closure (↑f ⁻¹' s) ≤ Submonoid.comap f (Submonoid.closure s)

theorem AddMonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) (s : Set M) : AddSubmonoid.map f (AddSubmonoid.closure s) = AddSubmonoid.closure (↑f '' s)

The image under an AddMonoid hom of the AddSubmonoid generated by a set equals the AddSubmonoid generated by the image of the set.

theorem MonoidHom.map_mclosure {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) (s : Set M) : Submonoid.map f (Submonoid.closure s) = Submonoid.closure (↑f '' s)

The image under a monoid hom of the submonoid generated by a set equals the submonoid generated by the image of the set.

def AddMonoidHom.restrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) : { x // x ∈ s } →+ N

Restriction of an AddMonoid hom to an AddSubmonoid of the domain.

def MonoidHom.restrict {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) : { x // x ∈ s } →* N

Restriction of a monoid hom to a submonoid of the domain.

@[simp]

theorem AddMonoidHom.restrict_apply {M : Type u_1} [AddZeroClass M] {N : Type u_6} {S : Type u_7} [AddZeroClass N] [SetLike S M] [AddSubmonoidClass S M] (f : M →+ N) (s : S) (x : { x // x ∈ s }) : ↑(AddMonoidHom.restrict f s) x = ↑f ↑x

@[simp]

theorem MonoidHom.restrict_apply {M : Type u_1} [MulOneClass M] {N : Type u_6} {S : Type u_7} [MulOneClass N] [SetLike S M] [SubmonoidClass S M] (f : M →* N) (s : S) (x : { x // x ∈ s }) : ↑(MonoidHom.restrict f s) x = ↑f ↑x

@[simp]

theorem AddMonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) : AddMonoidHom.mrange (AddMonoidHom.restrict f S) = AddSubmonoid.map f S

@[simp]

theorem MonoidHom.restrict_mrange {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) : MonoidHom.mrange (MonoidHom.restrict f S) = Submonoid.map f S

def AddMonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_6} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) : M →+ { x // x ∈ s }

Restriction of an AddMonoid hom to an AddSubmonoid of the codomain.

theorem AddMonoidHom.codRestrict.proof_1 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) : (fun n => { val := ↑f n, property := h n }) 0 = 0

theorem AddMonoidHom.codRestrict.proof_2 {M : Type u_3} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] {S : Type u_2} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) (x : M) (y : M) : ZeroHom.toFun { toFun := fun n => { val := ↑f n, property := h n }, map_zero' := (_ : (fun n => { val := ↑f n, property := h n }) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun n => { val := ↑f n, property := h n }, map_zero' := (_ : (fun n => { val := ↑f n, property := h n }) 0 = 0) } x + ZeroHom.toFun { toFun := fun n => { val := ↑f n, property := h n }, map_zero' := (_ : (fun n => { val := ↑f n, property := h n }) 0 = 0) } y

@[simp]

theorem AddMonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {S : Type u_6} [SetLike S N] [AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) (n : M) : ↑(AddMonoidHom.codRestrict f s h) n = { val := ↑f n, property := h n }

@[simp]

theorem MonoidHom.codRestrict_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) (n : M) : ↑(MonoidHom.codRestrict f s h) n = { val := ↑f n, property := h n }

def MonoidHom.codRestrict {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {S : Type u_6} [SetLike S N] [SubmonoidClass S N] (f : M →* N) (s : S) (h : ∀ (x : M), ↑f x ∈ s) : M →* { x // x ∈ s }

Restriction of a monoid hom to a submonoid of the codomain.

theorem AddMonoidHom.mrangeRestrict.proof_1 {M : Type u_1} [AddZeroClass M] {N : Type u_2} [AddZeroClass N] (f : M →+ N) (x : M) : ∃ y, ↑f y = ↑f x

def AddMonoidHom.mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} [AddZeroClass N] (f : M →+ N) : M →+ { x // x ∈ AddMonoidHom.mrange f }

Restriction of an AddMonoid hom to its range interpreted as a submonoid.

def MonoidHom.mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_6} [MulOneClass N] (f : M →* N) : M →* { x // x ∈ MonoidHom.mrange f }

Restriction of a monoid hom to its range interpreted as a submonoid.

@[simp]

theorem AddMonoidHom.coe_mrangeRestrict {M : Type u_1} [AddZeroClass M] {N : Type u_6} [AddZeroClass N] (f : M →+ N) (x : M) : ↑(↑(AddMonoidHom.mrangeRestrict f) x) = ↑f x

@[simp]

theorem MonoidHom.coe_mrangeRestrict {M : Type u_1} [MulOneClass M] {N : Type u_6} [MulOneClass N] (f : M →* N) (x : M) : ↑(↑(MonoidHom.mrangeRestrict f) x) = ↑f x

abbrev AddMonoidHom.mrangeRestrict_surjective.match_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (motive : { x // x ∈ AddMonoidHom.mrange f } → Prop) : (x : { x // x ∈ AddMonoidHom.mrange f }) → ((x : M) → motive { val := ↑f x, property := (_ : ∃ y, ↑f y = ↑f x) }) → motive x

theorem AddMonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : Function.Surjective ↑(AddMonoidHom.mrangeRestrict f)

theorem MonoidHom.mrangeRestrict_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) : Function.Surjective ↑(MonoidHom.mrangeRestrict f)

def AddMonoidHom.mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid M

The additive kernel of an AddMonoid hom is the AddSubmonoid of elements such that f x = 0

def MonoidHom.mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : Submonoid M

The multiplicative kernel of a monoid hom is the submonoid of elements x : G such that f x = 1

theorem AddMonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) {x : M} : x ∈ AddMonoidHom.mker f ↔ ↑f x = 0

theorem MonoidHom.mem_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) {x : M} : x ∈ MonoidHom.mker f ↔ ↑f x = 1

theorem AddMonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : ↑(AddMonoidHom.mker f) = ↑f ⁻¹' {0}

theorem MonoidHom.coe_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : ↑(MonoidHom.mker f) = ↑f ⁻¹' {1}

instance AddMonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] [DecidableEq N] (f : F) : DecidablePred fun x => x ∈ AddMonoidHom.mker f

instance MonoidHom.decidableMemMker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] [DecidableEq N] (f : F) : DecidablePred fun x => x ∈ MonoidHom.mker f

theorem AddMonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [AddZeroClass M] [AddZeroClass N] [AddZeroClass P] (g : N →+ P) (f : M →+ N) : AddSubmonoid.comap f (AddMonoidHom.mker g) = AddMonoidHom.mker (AddMonoidHom.comp g f)

theorem MonoidHom.comap_mker {M : Type u_1} {N : Type u_2} {P : Type u_3} [MulOneClass M] [MulOneClass N] [MulOneClass P] (g : N →* P) (f : M →* N) : Submonoid.comap f (MonoidHom.mker g) = MonoidHom.mker (MonoidHom.comp g f)

@[simp]

theorem AddMonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {F : Type u_5} [mc : AddMonoidHomClass F M N] (f : F) : AddSubmonoid.comap f ⊥ = AddMonoidHom.mker f

@[simp]

theorem MonoidHom.comap_bot' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {F : Type u_5} [mc : MonoidHomClass F M N] (f : F) : Submonoid.comap f ⊥ = MonoidHom.mker f

@[simp]

theorem AddMonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (f : M →+ N) : AddMonoidHom.mker (AddMonoidHom.restrict f S) = AddSubmonoid.comap (AddSubmonoid.subtype S) (AddMonoidHom.mker f)

@[simp]

theorem MonoidHom.restrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (f : M →* N) : MonoidHom.mker (MonoidHom.restrict f S) = Submonoid.comap (Submonoid.subtype S) (MonoidHom.mker f)

theorem AddMonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) : AddMonoidHom.mker (AddMonoidHom.mrangeRestrict f) = AddMonoidHom.mker f

theorem MonoidHom.mrangeRestrict_mker {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) : MonoidHom.mker (MonoidHom.mrangeRestrict f) = MonoidHom.mker f

@[simp]

theorem AddMonoidHom.mker_zero {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] : AddMonoidHom.mker 0 = ⊤

@[simp]

theorem MonoidHom.mker_one {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] : MonoidHom.mker 1 = ⊤

theorem AddMonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [