# mathlib3documentation

group_theory.submonoid.inverses

# Submonoid of inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given a submonoid N of a monoid M, we define the submonoid N.left_inv as the submonoid of left inverses of N. When M is commutative, we may define from_comm_left_inv : N.left_inv →* N since the inverses are unique. When N ≤ is_unit.submonoid M, this is precisely the pointwise inverse of N, and we may define left_inv_equiv : S.left_inv ≃* S.

For the pointwise inverse of submonoids of groups, please refer to group_theory.submonoid.pointwise.

## TODO #

Define the submonoid of right inverses and two-sided inverses. See the comments of #10679 for a possible implementation.

@[protected, instance]
noncomputable def submonoid.is_unit.submonoid.group {M : Type u_1} [monoid M] :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

S.left_neg is the additive submonoid containing all the left additive inverses of S.

Equations
def submonoid.left_inv {M : Type u_1} [monoid M] (S : submonoid M) :

S.left_inv is the submonoid containing all the left inverses of S.

Equations
theorem submonoid.left_inv_left_inv_le {M : Type u_1} [monoid M] (S : submonoid M) :
theorem submonoid.unit_mem_left_inv {M : Type u_1} [monoid M] (S : submonoid M) (x : Mˣ) (hx : x S) :
theorem submonoid.left_inv_left_inv_eq {M : Type u_1} [monoid M] (S : submonoid M) (hS : S ) :
theorem add_submonoid.left_neg_left_neg_eq {M : Type u_1} [add_monoid M] (S : add_submonoid M) (hS : S ) :

The function from S.left_add to S sending an element to its right additive inverse in S. This is an add_monoid_hom when M is commutative.

Equations
noncomputable def submonoid.from_left_inv {M : Type u_1} [monoid M] (S : submonoid M) :

The function from S.left_inv to S sending an element to its right inverse in S. This is a monoid_hom when M is commutative.

Equations
@[simp]
@[simp]
theorem submonoid.mul_from_left_inv {M : Type u_1} [monoid M] (S : submonoid M) (x : (S.left_inv)) :
@[simp]
= 0
@[simp]
theorem submonoid.from_left_inv_one {M : Type u_1} [monoid M] (S : submonoid M) :
= 1
@[simp]
theorem submonoid.from_left_inv_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (x : (S.left_inv)) :
@[simp]
theorem add_submonoid.from_left_neg_eq_iff {M : Type u_1} (S : add_submonoid M) (a : (S.left_neg)) (b : M) :
(S.from_left_neg a) = b a + b = 0
theorem submonoid.from_left_inv_eq_iff {M : Type u_1} [comm_monoid M] (S : submonoid M) (a : (S.left_inv)) (b : M) :
(S.from_left_inv a) = b a * b = 1
@[simp]
noncomputable def add_submonoid.from_comm_left_neg {M : Type u_1} (S : add_submonoid M) :

The add_monoid_hom from S.left_neg to S sending an element to its right additive inverse in S.

Equations
noncomputable def submonoid.from_comm_left_inv {M : Type u_1} [comm_monoid M] (S : submonoid M) :

The monoid_hom from S.left_inv to S sending an element to its right inverse in S.

Equations
@[simp]
theorem submonoid.from_comm_left_inv_apply {M : Type u_1} [comm_monoid M] (S : submonoid M) (ᾰ : (S.left_inv)) :
noncomputable def submonoid.left_inv_equiv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) :

The submonoid of pointwise inverse of S is mul_equiv to S.

Equations
@[simp]
theorem add_submonoid.left_neg_equiv_apply {M : Type u_1} (S : add_submonoid M) (hS : S ) (ᾰ : (S.left_neg)) :
(S.left_neg_equiv hS) =
noncomputable def add_submonoid.left_neg_equiv {M : Type u_1} (S : add_submonoid M) (hS : S ) :

Equations
@[simp]
theorem submonoid.left_inv_equiv_apply {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (ᾰ : (S.left_inv)) :
(S.left_inv_equiv hS) =
@[simp]
theorem add_submonoid.from_left_neg_left_neg_equiv_symm {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : S) :
@[simp]
theorem submonoid.from_left_inv_left_inv_equiv_symm {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : S) :
@[simp]
theorem add_submonoid.left_neg_equiv_symm_from_left_neg {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : (S.left_neg)) :
@[simp]
theorem submonoid.left_inv_equiv_symm_from_left_inv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : (S.left_inv)) :
theorem add_submonoid.left_neg_equiv_add {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : (S.left_neg)) :
((S.left_neg_equiv hS) x) + x = 0
theorem submonoid.left_inv_equiv_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : (S.left_inv)) :
((S.left_inv_equiv hS) x) * x = 1
theorem add_submonoid.add_left_neg_equiv {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : (S.left_neg)) :
x + ((S.left_neg_equiv hS) x) = 0
theorem submonoid.mul_left_inv_equiv {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : (S.left_inv)) :
x * ((S.left_inv_equiv hS) x) = 1
@[simp]
theorem submonoid.left_inv_equiv_symm_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : S) :
(((S.left_inv_equiv hS).symm) x) * x = 1
@[simp]
theorem add_submonoid.left_neg_equiv_symm_add {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : S) :
(((S.left_neg_equiv hS).symm) x) + x = 0
@[simp]
theorem add_submonoid.add_left_neg_equiv_symm {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : S) :
x + (((S.left_neg_equiv hS).symm) x) = 0
@[simp]
theorem submonoid.mul_left_inv_equiv_symm {M : Type u_1} [comm_monoid M] (S : submonoid M) (hS : S ) (x : S) :
x * (((S.left_inv_equiv hS).symm) x) = 1
theorem submonoid.left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) :
@[simp]
@[simp]
theorem submonoid.from_left_inv_eq_inv {M : Type u_1} [group M] (S : submonoid M) (x : (S.left_inv)) :
@[simp]
theorem submonoid.left_inv_equiv_symm_eq_inv {M : Type u_1} [comm_group M] (S : submonoid M) (hS : S ) (x : S) :
@[simp]
theorem add_submonoid.left_neg_equiv_symm_eq_neg {M : Type u_1} (S : add_submonoid M) (hS : S ) (x : S) :