Documentation

Mathlib.GroupTheory.Submonoid.Operations

Operations on Submonoids #

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

Main definitions #

Conversion between multiplicative and additive definitions #

(Commutative) monoid structure on a submonoid #

Group actions by submonoids #

Operations on submonoids #

Monoid homomorphisms between submonoid #

Operations on MonoidHoms #

Tags #

submonoid, range, product, map, comap

Conversion to/from Additive/Multiplicative #

@[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

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]

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

Equations
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

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]

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

Equations
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) :

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

Equations
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 ⁻¹' Sb f ⁻¹' Sf (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) :

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

Equations
@[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) :
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) :
@[simp]
theorem Submonoid.comap_id {P : Type u_1} [inst : MulOneClass P] (S : Submonoid P) :
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 '' Sb f '' Sa + b f '' S
Equations
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) :

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) :

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) :
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) :
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) :
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} :
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} :
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) :
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) :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
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} :
@[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} :
@[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} :
@[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} :
@[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} :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[simp]
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) SProp) (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) :
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) :
Equations
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) :

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) :

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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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} :
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} :
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) :
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) :
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) :
Equations
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) :

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
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) :

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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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} :
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} :
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) :
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) :
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
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
@[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
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
@[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
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
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
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
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
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
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
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
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
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) :

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
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
Equations
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
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) :

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
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
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
instance SubmonoidClass.toLinearOrderedCommMonoid {M : Type u_1} [inst : LinearOrderedCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

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
instance AddSubmonoidClass.toOrderedCancelAddCommMonoid {M : Type u_1} [inst : OrderedCancelAddCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : AddSubmonoidClass A M] (S : A) :

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
instance SubmonoidClass.toOrderedCancelCommMonoid {M : Type u_1} [inst : OrderedCancelCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

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))

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
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
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
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
instance SubmonoidClass.toLinearOrderedCancelCommMonoid {M : Type u_1} [inst : LinearOrderedCancelCommMonoid M] {A : Type u_2} [inst : SetLike A M] [inst : SubmonoidClass A M] (S : A) :

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
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
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
@[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) }
Equations
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
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
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
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_5 {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) :
∀ (x : { x // x S }) (x_1 : ), ↑(x_1 x) = ↑(x_1 x)
Equations
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.
Equations
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
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.

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
Equations
  • (_ : 0 = 0) = (_ : 0 = 0)
Equations
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_7 {M : Type u_1} [inst : LinearOrderedAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
Equations
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
Equations
  • (_ : 0 = 0) = (_ : 0 = 0)
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

An AddSubmonoid of a LinearOrderedAddCommMonoid is a LinearOrderedAddCommMonoid.

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

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))
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

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

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

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_7 {M : Type u_1} [inst : LinearOrderedCancelAddCommMonoid M] (S : AddSubmonoid M) :
∀ (x x_1 : { x // x S }), ↑(x x_1) = ↑(x x_1)
Equations
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
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))
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

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.
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} :
@[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) :

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
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 ×ˢ tb s ×ˢ t(a + b).fst s (a + b).snd t
Equations
def Submonoid.prod {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) (t : Submonoid 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₂) :
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 Submonoid.prod_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) :
theorem Submonoid.top_prod {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid N) :
@[simp]
theorem AddSubmonoid.top_prod_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] :
@[simp]
theorem Submonoid.top_prod_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
theorem Submonoid.bot_prod_bot {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] :
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
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
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) sProp) :
(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
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
theorem Submonoid.map_inl {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid M) :
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 sProp) :
(x : p AddSubmonoid.prod s) → ((hp1 : p.fst ) → (hps : p.snd s) → motive (_ : p.fst p.snd s)) → motive x
Equations
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) sProp) :
(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
theorem Submonoid.map_inr {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst : MulOneClass N] (s : Submonoid N) :
@[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) :
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} :
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} :
@[simp]
theorem AddSubmonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst : AddZeroClass N] (f : M ≃+ N) :
@[simp]
theorem Submonoid.map_equiv_top {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] (f : M ≃* N) :
theorem Submonoid.le_prod_iff {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst : MulOneClass N] {s : Submonoid M} {t : Submonoid N}