Documentation

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

Equations

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

Instances For

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

Equations

AddSubmonoid.toSubmonoid' = OrderIso.symm Submonoid.toAddSubmonoid

Instances For

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.

Equations

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

Instances For

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

Equations

Submonoid.toAddSubmonoid' = OrderIso.symm AddSubmonoid.toSubmonoid

Instances For

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.

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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.

Equations

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

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.

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

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.

Equations

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

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

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.

Equations

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

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.

Equations

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

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

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.

Equations

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

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.

Equations

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

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.

Equations

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

theorem AddSubmonoidClass.toOrderedAddCommMonoid.proof_1 {M : Type u_1} [OrderedAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass 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.

Equations

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

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.

Equations

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

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

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.

Equations

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

theorem AddSubmonoidClass.toOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [OrderedCancelAddCommMonoid M] {A : Type u_2} [SetLike A M] [AddSubmonoidClass 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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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.

Equations

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

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.

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

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.

Equations

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

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

Zero { x // x ∈ S }

An AddSubmonoid of an AddMonoid inherits a zero.

Equations

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

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

One { x // x ∈ S }

A submonoid of a monoid inherits a 1.

Equations

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

@[simp]

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

Equations

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

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.

Equations

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

theorem AddSubmonoid.nsmul_mem {M : Type u_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.

Equations

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

theorem AddSubmonoid.toAddMonoid.proof_1 {M : Type u_1} [AddMonoid 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.

Equations

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

theorem AddSubmonoid.toAddCommMonoid.proof_1 {M : Type u_1} [AddCommMonoid 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.

Equations

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

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.

Equations

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

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.

Equations

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

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

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.

Equations

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

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

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.

Equations

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

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

LinearOrderedCommMonoid { x // x ∈ S }

A submonoid of a LinearOrderedCommMonoid is a LinearOrderedCommMonoid.

Equations

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

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

OrderedCancelAddCommMonoid { x // x ∈ S }

An AddSubmonoid of an OrderedCancelAddCommMonoid is an OrderedCancelAddCommMonoid.

Equations

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

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

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.

Equations

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

theorem AddSubmonoid.toLinearOrderedCancelAddCommMonoid.proof_1 {M : Type u_1} [LinearOrderedCancelAddCommMonoid 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.

Equations

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

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.

Equations

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

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.

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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.

Equations

AddMonoidHom.mrange f = AddSubmonoid.copy (AddSubmonoid.map f ⊤) (Set.range ↑f) (_ : Set.range ↑f = ↑f '' Set.univ)

Instances For

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].

Equations

MonoidHom.mrange f = Submonoid.copy (Submonoid.map f ⊤) (Set.range ↑f) (_ : Set.range ↑f = ↑f '' Set.univ)

Instances For

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

Equations

AddMonoidHom.restrict f s = AddMonoidHom.comp f (AddSubmonoidClass.subtype s)

Instances For

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.

Equations

MonoidHom.restrict f s = MonoidHom.comp f (SubmonoidClass.subtype s)

Instances For

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

Equations

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

Instances For

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.

Equations

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

Instances For

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.

Equations

AddMonoidHom.mrangeRestrict f = AddMonoidHom.codRestrict f (AddMonoidHom.mrange f) (_ : ∀ (x : M), ∃ y, ↑f y = ↑f x)

Instances For

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.

Equations

MonoidHom.mrangeRestrict f = MonoidHom.codRestrict f (MonoidHom.mrange f) (_ : ∀ (x : M), ∃ y, ↑f y = ↑f x)

Instances For

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

Equations

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

Instances For

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

Equations

AddMonoidHom.mker f = AddSubmonoid.comap f ⊥

Instances For

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

Equations

MonoidHom.mker f = Submonoid.comap f ⊥

Instances For

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

Equations

AddMonoidHom.decidableMemMker f x = decidable_of_iff (↑f x = 0) (_ : x ∈ AddMonoidHom.mker f ↔ ↑f x = 0)

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

Equations

MonoidHom.decidableMemMker f x = decidable_of_iff (↑f x = 1) (_ : x ∈ MonoidHom.mker f ↔ ↑f x = 1)

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'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') (S : AddSubmonoid N) (S' : AddSubmonoid N') :

AddSubmonoid.comap (AddMonoidHom.prodMap f g) (AddSubmonoid.prod S S') = AddSubmonoid.prod (AddSubmonoid.comap f S) (AddSubmonoid.comap g S')

theorem MonoidHom.prod_map_comap_prod' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') (S : Submonoid N) (S' : Submonoid N') :

Submonoid.comap (MonoidHom.prodMap f g) (Submonoid.prod S S') = Submonoid.prod (Submonoid.comap f S) (Submonoid.comap g S')

theorem AddMonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] {M' : Type u_6} {N' : Type u_7} [AddZeroClass M'] [AddZeroClass N'] (f : M →+ N) (g : M' →+ N') :

AddMonoidHom.mker (AddMonoidHom.prodMap f g) = AddSubmonoid.prod (AddMonoidHom.mker f) (AddMonoidHom.mker g)

theorem MonoidHom.mker_prod_map {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {M' : Type u_6} {N' : Type u_7} [MulOneClass M'] [MulOneClass N'] (f : M →* N) (g : M' →* N') :

MonoidHom.mker (MonoidHom.prodMap f g) = Submonoid.prod (MonoidHom.mker f) (MonoidHom.mker g)

@[simp]

theorem AddMonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.inl M N) = ⊥

@[simp]

theorem MonoidHom.mker_inl {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.inl M N) = ⊥

@[simp]

theorem AddMonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.inr M N) = ⊥

@[simp]

theorem MonoidHom.mker_inr {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.inr M N) = ⊥

@[simp]

theorem AddMonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.fst M N) = AddSubmonoid.prod ⊥ ⊤

@[simp]

theorem MonoidHom.mker_fst {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.fst M N) = Submonoid.prod ⊥ ⊤

@[simp]

theorem AddMonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mker (AddMonoidHom.snd M N) = AddSubmonoid.prod ⊤ ⊥

@[simp]

theorem MonoidHom.mker_snd {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mker (MonoidHom.snd M N) = Submonoid.prod ⊤ ⊥

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

{ x // x ∈ AddSubmonoid.comap f N' } →+ { x // x ∈ N' }

the AddMonoidHom from the preimage of an additive submonoid to itself.

Equations

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

Instances For

theorem AddMonoidHom.addSubmonoidComap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : { x // x ∈ AddSubmonoid.comap f N' }) :

↑x ∈ AddSubmonoid.comap f N'

theorem AddMonoidHom.addSubmonoidComap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : { x // x ∈ AddSubmonoid.comap f N' }) (y : { x // x ∈ AddSubmonoid.comap f N' }) :

ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }) 0 = 0) } x + ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }) 0 = 0) } y

theorem AddMonoidHom.addSubmonoidComap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) :

(fun x => { val := ↑f ↑x, property := (_ : ↑x ∈ AddSubmonoid.comap f N') }) 0 = 0

@[simp]

theorem AddMonoidHom.addSubmonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (N' : AddSubmonoid N) (x : { x // x ∈ AddSubmonoid.comap f N' }) :

↑(↑(AddMonoidHom.addSubmonoidComap f N') x) = ↑f ↑x

@[simp]

theorem MonoidHom.submonoidComap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (N' : Submonoid N) (x : { x // x ∈ Submonoid.comap f N' }) :

↑(↑(MonoidHom.submonoidComap f N') x) = ↑f ↑x

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

{ x // x ∈ Submonoid.comap f N' } →* { x // x ∈ N' }

The MonoidHom from the preimage of a submonoid to itself.

Equations

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

Instances For

theorem AddMonoidHom.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : { x // x ∈ M' }) (y : { x // x ∈ M' }) :

ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) 0 = 0) } (x + y) = ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) 0 = 0) } x + ZeroHom.toFun { toFun := fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }, map_zero' := (_ : (fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) 0 = 0) } y

theorem AddMonoidHom.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : { x // x ∈ M' }) :

∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x

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

{ x // x ∈ M' } →+ { x // x ∈ AddSubmonoid.map f M' }

the AddMonoidHom from an additive submonoid to its image. See AddEquiv.AddSubmonoidMap for a variant for AddEquivs.

Equations

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

Instances For

theorem AddMonoidHom.addSubmonoidMap.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :

(fun x => { val := ↑f ↑x, property := (_ : ∃ a, a ∈ ↑M' ∧ ↑f a = ↑f ↑x) }) 0 = 0

@[simp]

theorem AddMonoidHom.addSubmonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) (x : { x // x ∈ M' }) :

↑(↑(AddMonoidHom.addSubmonoidMap f M') x) = ↑f ↑x

@[simp]

theorem MonoidHom.submonoidMap_apply_coe {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) (x : { x // x ∈ M' }) :

↑(↑(MonoidHom.submonoidMap f M') x) = ↑f ↑x

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

{ x // x ∈ M' } →* { x // x ∈ Submonoid.map f M' }

The MonoidHom from a submonoid to its image. See MulEquiv.SubmonoidMap for a variant for MulEquivs.

Equations

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

Instances For

theorem AddMonoidHom.addSubmonoidMap_surjective {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M) :

Function.Surjective ↑(AddMonoidHom.addSubmonoidMap f M')

theorem MonoidHom.submonoidMap_surjective {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) (M' : Submonoid M) :

Function.Surjective ↑(MonoidHom.submonoidMap f M')

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

AddMonoidHom.mrange (AddMonoidHom.inl M N) = AddSubmonoid.prod ⊤ ⊥

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

MonoidHom.mrange (MonoidHom.inl M N) = Submonoid.prod ⊤ ⊥

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

AddMonoidHom.mrange (AddMonoidHom.inr M N) = AddSubmonoid.prod ⊥ ⊤

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

MonoidHom.mrange (MonoidHom.inr M N) = Submonoid.prod ⊥ ⊤

theorem AddSubmonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inl M N) = AddSubmonoid.comap (AddMonoidHom.snd M N) ⊥

theorem Submonoid.mrange_inl' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inl M N) = Submonoid.comap (MonoidHom.snd M N) ⊥

theorem AddSubmonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] :

AddMonoidHom.mrange (AddMonoidHom.inr M N) = AddSubmonoid.comap (AddMonoidHom.fst M N) ⊥

theorem Submonoid.mrange_inr' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] :

MonoidHom.mrange (MonoidHom.inr M N) = Submonoid.comap (MonoidHom.fst M N) ⊥

@[simp]

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

AddMonoidHom.mrange (AddMonoidHom.fst M N) = ⊤

@[simp]

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

MonoidHom.mrange (MonoidHom.fst M N) = ⊤

@[simp]

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

AddMonoidHom.mrange (AddMonoidHom.snd M N) = ⊤

@[simp]

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

MonoidHom.mrange (MonoidHom.snd M N) = ⊤

theorem AddSubmonoid.prod_eq_bot_iff {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.prod_eq_bot_iff {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.prod_eq_top_iff {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.prod_eq_top_iff {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] {s : Submonoid M} {t : Submonoid N} :

Submonoid.prod s t = ⊤ ↔ s = ⊤ ∧ t = ⊤

@[simp]

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

AddMonoidHom.mrange (AddMonoidHom.inl M N) ⊔ AddMonoidHom.mrange (AddMonoidHom.inr M N) = ⊤

@[simp]

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

MonoidHom.mrange (MonoidHom.inl M N) ⊔ MonoidHom.mrange (MonoidHom.inr M N) = ⊤

def AddSubmonoid.inclusion {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S ≤ T) :

{ x // x ∈ S } →+ { x // x ∈ T }

The AddMonoid hom associated to an inclusion of submonoids.

Equations

AddSubmonoid.inclusion h = AddMonoidHom.codRestrict (AddSubmonoid.subtype S) T (_ : ∀ (x : { x // x ∈ S }), ↑(AddSubmonoid.subtype S) x ∈ T)

Instances For

theorem AddSubmonoid.inclusion.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S ≤ T) (x : { x // x ∈ S }) :

↑(AddSubmonoid.subtype S) x ∈ T

def Submonoid.inclusion {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S ≤ T) :

{ x // x ∈ S } →* { x // x ∈ T }

The monoid hom associated to an inclusion of submonoids.

Equations

Submonoid.inclusion h = MonoidHom.codRestrict (Submonoid.subtype S) T (_ : ∀ (x : { x // x ∈ S }), ↑(Submonoid.subtype S) x ∈ T)

Instances For

@[simp]

theorem AddSubmonoid.range_subtype {M : Type u_1} [AddZeroClass M] (s : AddSubmonoid M) :

AddMonoidHom.mrange (AddSubmonoid.subtype s) = s

@[simp]

theorem Submonoid.range_subtype {M : Type u_1} [MulOneClass M] (s : Submonoid M) :

MonoidHom.mrange (Submonoid.subtype s) = s

theorem AddSubmonoid.eq_top_iff' {M : Type u_1} [AddZeroClass M] (S : AddSubmonoid M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

theorem Submonoid.eq_top_iff' {M : Type u_1} [MulOneClass M] (S : Submonoid M) :

S = ⊤ ↔ ∀ (x : M), x ∈ S

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

S = ⊥ ↔ ∀ (x : M), x ∈ S → x = 0

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

S = ⊥ ↔ ∀ (x : M), x ∈ S → x = 1

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

Nontrivial { x // x ∈ S } ↔ ∃ x, x ∈ S ∧ x ≠ 0

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

Nontrivial { x // x ∈ S } ↔ ∃ x, x ∈ S ∧ x ≠ 1

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

S = ⊥ ∨ Nontrivial { x // x ∈ S }

An additive submonoid is either the trivial additive submonoid or nontrivial.

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

S = ⊥ ∨ Nontrivial { x // x ∈ S }

A submonoid is either the trivial submonoid or nontrivial.

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

S = ⊥ ∨ ∃ x, x ∈ S ∧ x ≠ 0

An additive submonoid is either the trivial additive submonoid or contains a nonzero element.

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

S = ⊥ ∨ ∃ x, x ∈ S ∧ x ≠ 1

A submonoid is either the trivial submonoid or contains a nonzero element.

def AddEquiv.addSubmonoidCongr {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

{ x // x ∈ S } ≃+ { x // x ∈ T }

Makes the identity additive isomorphism from a proof two submonoids of an additive monoid are equal.

Equations

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

Instances For

theorem AddEquiv.addSubmonoidCongr.proof_1 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

↑S = ↑T

theorem AddEquiv.addSubmonoidCongr.proof_3 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

Function.RightInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun

theorem AddEquiv.addSubmonoidCongr.proof_2 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

Function.LeftInverse (Equiv.setCongr (_ : ↑S = ↑T)).invFun (Equiv.setCongr (_ : ↑S = ↑T)).toFun

theorem AddEquiv.addSubmonoidCongr.proof_4 {M : Type u_1} [AddZeroClass M] {S : AddSubmonoid M} {T : AddSubmonoid M} (h : S = T) :

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

def MulEquiv.submonoidCongr {M : Type u_1} [MulOneClass M] {S : Submonoid M} {T : Submonoid M} (h : S = T) :

{ x // x ∈ S } ≃* { x // x ∈ T }

Makes the identity isomorphism from a proof that two submonoids of a multiplicative monoid are equal.

Equations

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

Instances For

theorem AddEquiv.ofLeftInverse'.proof_1 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ↑f) (x : { x // x ∈ AddMonoidHom.mrange f }) :

↑(AddMonoidHom.mrangeRestrict f) ((g ∘ ↑(AddSubmonoid.subtype (AddMonoidHom.mrange f))) x) = x

def AddEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ↑f) :

M ≃+ { x // x ∈ AddMonoidHom.mrange f }

An additive monoid homomorphism f : M →+ N with a left-inverse g : N → M defines an additive equivalence between M and f.mrange. This is a bidirectional version of AddMonoidHom.mrange_restrict.

Equations

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

Instances For

abbrev AddEquiv.ofLeftInverse'.match_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : { x // x ∈ AddMonoidHom.mrange f }) (motive : (∃ x, ↑f x = ↑x) → Prop) :

(x : ∃ x, ↑f x = ↑x) → ((x' : M) → (hx' : ↑f x' = ↑x) → motive (_ : ∃ x, ↑f x = ↑x)) → motive x

Equations

AddEquiv.ofLeftInverse'.match_1 f x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

Instances For

theorem AddEquiv.ofLeftInverse'.proof_2 {M : Type u_2} {N : Type u_1} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) (x : M) (y : M) :

ZeroHom.toFun (↑(AddMonoidHom.mrangeRestrict f)) (x + y) = ZeroHom.toFun (↑(AddMonoidHom.mrangeRestrict f)) x + ZeroHom.toFun (↑(AddMonoidHom.mrangeRestrict f)) y

@[simp]

theorem MulEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ↑f) :

∀ (a : { x // x ∈ MonoidHom.mrange f }), ↑(MulEquiv.symm (MulEquiv.ofLeftInverse' f h)) a = g ↑a

@[simp]

theorem AddEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ↑f) (a : M) :

↑(AddEquiv.ofLeftInverse' f h) a = ↑(AddMonoidHom.mrangeRestrict f) a

@[simp]

theorem MulEquiv.ofLeftInverse'_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ↑f) (a : M) :

↑(MulEquiv.ofLeftInverse' f h) a = ↑(MonoidHom.mrangeRestrict f) a

@[simp]

theorem AddEquiv.ofLeftInverse'_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (f : M →+ N) {g : N → M} (h : Function.LeftInverse g ↑f) :

∀ (a : { x // x ∈ AddMonoidHom.mrange f }), ↑(AddEquiv.symm (AddEquiv.ofLeftInverse' f h)) a = g ↑a

def MulEquiv.ofLeftInverse' {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (f : M →* N) {g : N → M} (h : Function.LeftInverse g ↑f) :

M ≃* { x // x ∈ MonoidHom.mrange f }

A monoid homomorphism f : M →* N with a left-inverse g : N → M defines a multiplicative equivalence between M and f.mrange. This is a bidirectional version of MonoidHom.mrange_restrict.

Equations

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

Instances For

theorem AddEquiv.addSubmonoidMap.proof_2 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :

Function.RightInverse (Equiv.image ↑e ↑S).invFun (Equiv.image ↑e ↑S).toFun

def AddEquiv.addSubmonoidMap {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :

{ x // x ∈ S } ≃+ { x // x ∈ AddSubmonoid.map (AddEquiv.toAddMonoidHom e) S }

An AddEquiv φ between two additive monoids M and N induces an AddEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See AddMonoidHom.addSubmonoidMap for a variant for AddMonoidHoms.

Equations

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

Instances For

theorem AddEquiv.addSubmonoidMap.proof_1 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :

Function.LeftInverse (Equiv.image ↑e ↑S).invFun (Equiv.image ↑e ↑S).toFun

theorem AddEquiv.addSubmonoidMap.proof_3 {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) :

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

def MulEquiv.submonoidMap {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) :

{ x // x ∈ S } ≃* { x // x ∈ Submonoid.map (MulEquiv.toMonoidHom e) S }

A MulEquiv φ between two monoids M and N induces a MulEquiv between a submonoid S ≤ M and the submonoid φ(S) ≤ N. See MonoidHom.submonoidMap for a variant for MonoidHoms.

Equations

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

Instances For

@[simp]

theorem AddEquiv.coe_addSubmonoidMap_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : { x // x ∈ S }) :

↑(↑(AddEquiv.addSubmonoidMap e S) g) = ↑e ↑g

@[simp]

theorem MulEquiv.coe_submonoidMap_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : { x // x ∈ S }) :

↑(↑(MulEquiv.submonoidMap e S) g) = ↑e ↑g

@[simp]

theorem AddEquiv.add_submonoid_map_symm_apply {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (e : M ≃+ N) (S : AddSubmonoid M) (g : { x // x ∈ AddSubmonoid.map (↑e) S }) :

↑(AddEquiv.symm (AddEquiv.addSubmonoidMap e S)) g = { val := ↑(AddEquiv.symm e) ↑g, property := (_ : ↑(AddEquiv.symm e) ↑g ∈ S) }

@[simp]

theorem MulEquiv.submonoidMap_symm_apply {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : { x // x ∈ Submonoid.map (↑e) S }) :

↑(MulEquiv.symm (MulEquiv.submonoidMap e S)) g = { val := ↑(MulEquiv.symm e) ↑g, property := (_ : ↑(MulEquiv.symm e) ↑g ∈ S) }

@[simp]

theorem AddSubmonoid.equivMapOfInjective_coe_addEquiv {M : Type u_1} {N : Type u_2} [AddZeroClass M] [AddZeroClass N] (S : AddSubmonoid M) (e : M ≃+ N) :

AddSubmonoid.equivMapOfInjective S ↑e (_ : Function.Injective ↑e) = AddEquiv.addSubmonoidMap e S

@[simp]

theorem Submonoid.equivMapOfInjective_coe_mulEquiv {M : Type u_1} {N : Type u_2} [MulOneClass M] [MulOneClass N] (S : Submonoid M) (e : M ≃* N) :

Submonoid.equivMapOfInjective S ↑e (_ : Function.Injective ↑e) = MulEquiv.submonoidMap e S

Actions by `Submonoid`s #

These instances transfer the action by an element m : M of a monoid M written as m • a onto the action by an element s : S of a submonoid S : Submonoid M such that s • a = (s : M) • a.

These instances work particularly well in conjunction with Monoid.toMulAction, enabling s • m as an alias for ↑s * m.

instance AddSubmonoid.vadd {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] (S : AddSubmonoid M') :

VAdd { x // x ∈ S } α

Equations

AddSubmonoid.vadd S = VAdd.comp α ↑(AddSubmonoid.subtype S)

instance Submonoid.smul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] (S : Submonoid M') :

SMul { x // x ∈ S } α

Equations

Submonoid.smul S = SMul.comp α ↑(Submonoid.subtype S)

instance AddSubmonoid.vaddCommClass_left {M' : Type u_5} {α : Type u_6} {β : Type u_7} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') :

VAddCommClass { x // x ∈ S } α β

Equations

@AddSubmonoid.vaddCommClass_left = @AddSubmonoid.vaddCommClass_left.proof_1

theorem AddSubmonoid.vaddCommClass_left.proof_1 {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd M' β] [VAdd α β] [VAddCommClass M' α β] (S : AddSubmonoid M') :

VAddCommClass { x // x ∈ S } α β

instance Submonoid.smulCommClass_left {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul M' β] [SMul α β] [SMulCommClass M' α β] (S : Submonoid M') :

SMulCommClass { x // x ∈ S } α β

Equations

@Submonoid.smulCommClass_left = @Submonoid.smulCommClass_left.proof_1

theorem AddSubmonoid.vaddCommClass_right.proof_1 {M' : Type u_1} {α : Type u_2} {β : Type u_3} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') :

VAddCommClass α { x // x ∈ S } β

instance AddSubmonoid.vaddCommClass_right {M' : Type u_5} {α : Type u_6} {β : Type u_7} [AddZeroClass M'] [VAdd α β] [VAdd M' β] [VAddCommClass α M' β] (S : AddSubmonoid M') :

VAddCommClass α { x // x ∈ S } β

Equations

@AddSubmonoid.vaddCommClass_right = @AddSubmonoid.vaddCommClass_right.proof_1

instance Submonoid.smulCommClass_right {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul α β] [SMul M' β] [SMulCommClass α M' β] (S : Submonoid M') :

SMulCommClass α { x // x ∈ S } β

Equations

@Submonoid.smulCommClass_right = @Submonoid.smulCommClass_right.proof_1

instance Submonoid.isScalarTower {M' : Type u_5} {α : Type u_6} {β : Type u_7} [MulOneClass M'] [SMul α β] [SMul M' α] [SMul M' β] [IsScalarTower M' α β] (S : Submonoid M') :

IsScalarTower { x // x ∈ S } α β

Note that this provides IsScalarTower S M' M' which is needed by SMulMulAssoc.

Equations

@Submonoid.isScalarTower = @Submonoid.isScalarTower.proof_1

theorem AddSubmonoid.vadd_def {M' : Type u_5} {α : Type u_6} [AddZeroClass M'] [VAdd M' α] {S : AddSubmonoid M'} (g : { x // x ∈ S }) (m : α) :

g +ᵥ m = ↑g +ᵥ m

theorem Submonoid.smul_def {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] {S : Submonoid M'} (g : { x // x ∈ S }) (m : α) :

g • m = ↑g • m

instance Submonoid.faithfulSMul {M' : Type u_5} {α : Type u_6} [MulOneClass M'] [SMul M' α] [FaithfulSMul M' α] (S : Submonoid M') :

FaithfulSMul { x // x ∈ S } α

Equations

@Submonoid.faithfulSMul = @Submonoid.faithfulSMul.proof_1

instance AddSubmonoid.addAction {M' : Type u_5} {α : Type u_6} [AddMonoid M'] [AddAction M' α] (S : AddSubmonoid M') :

AddAction { x // x ∈ S } α

The additive action by an AddSubmonoid is the action by the underlying AddMonoid.

Equations

AddSubmonoid.addAction S = AddAction.compHom α (AddSubmonoid.subtype S)

instance Submonoid.mulAction {M' : Type u_5} {α : Type u_6} [Monoid M'] [MulAction M' α] (S : Submonoid M') :

MulAction { x // x ∈ S } α

The action by a submonoid is the action by the underlying monoid.

Equations

Submonoid.mulAction S = MulAction.compHom α (Submonoid.subtype S)

instance Submonoid.distribMulAction {M' : Type u_5} {α : Type u_6} [Monoid M'] [AddMonoid α] [DistribMulAction M' α] (S : Submonoid M') :

DistribMulAction { x // x ∈ S } α

The action by a submonoid is the action by the underlying monoid.

Equations

Submonoid.distribMulAction S = DistribMulAction.compHom α (Submonoid.subtype S)