# Documentation

Mathlib.GroupTheory.Submonoid.Inverses

# Submonoid of inverses #

Given a submonoid N of a monoid M, we define the submonoid N.leftInv as the submonoid of left inverses of N. When M is commutative, we may define fromCommLeftInv : N.leftInv →* N since the inverses are unique. When N ≤ IsUnit.Submonoid M, this is precisely the pointwise inverse of N, and we may define leftInvEquiv : S.leftInv ≃* S.

For the pointwise inverse of submonoids of groups, please refer to GroupTheory.Submonoid.Pointwise.

## TODO #

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

(fun n x => n x) (n + 1) x = x + (fun n x => n x) n x
theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [] (x : { x // }) :
theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [] (x : { x // }) :
x⁻¹ = (IsUnit.unit (_ : ))⁻¹
theorem AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [] (S : ) {a : M} (_b : M) :
a {x | y, x + y = 0}_b {x | y, x + y = 0}a + _b {x | y, x + y = 0}
def AddSubmonoid.leftNeg {M : Type u_1} [] (S : ) :

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

Instances For
abbrev AddSubmonoid.leftNeg.match_1 {M : Type u_1} [] (S : ) (_b : M) (motive : _b {x | y, x + y = 0}Prop) :
(x : _b {x | y, x + y = 0}) → ((b' : { x // x S }) → (hb : _b + b' = 0) → motive (_ : y, _b + y = 0)) → motive x
Instances For
theorem AddSubmonoid.leftNeg.proof_2 {M : Type u_1} [] (S : ) :
y, 0 + y = 0
def Submonoid.leftInv {M : Type u_1} [] (S : ) :

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

Instances For
theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [] (S : ) :
theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [] (S : ) :
theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [] (S : ) (x : ) (hx : x S) :
↑(-x)
theorem Submonoid.unit_mem_leftInv {M : Type u_1} [] (S : ) (x : Mˣ) (hx : x S) :
theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [] (S : ) (hS : ) :
theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [] (S : ) (hS : ) :
theorem AddSubmonoid.fromLeftNeg.proof_1 {M : Type u_1} [] (S : ) (x : { x // }) :
noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [] (S : ) :
{ x // }{ x // x S }

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

Instances For
noncomputable def Submonoid.fromLeftInv {M : Type u_1} [] (S : ) :
{ x // }{ x // x S }

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

Instances For
@[simp]
theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [] (S : ) (x : { x // }) :
x + ↑() = 0
@[simp]
theorem Submonoid.mul_fromLeftInv {M : Type u_1} [] (S : ) (x : { x // }) :
x * ↑() = 1
@[simp]
theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [] (S : ) :
@[simp]
theorem Submonoid.fromLeftInv_one {M : Type u_1} [] (S : ) :
@[simp]
theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [] (S : ) (x : { x // }) :
↑() + x = 0
@[simp]
theorem Submonoid.fromLeftInv_mul {M : Type u_1} [] (S : ) (x : { x // }) :
↑() * x = 1
abbrev AddSubmonoid.leftNeg_le_isAddUnit.match_1 {M : Type u_1} [] (S : ) (x : M) (motive : ) :
(x : ) → ((y : { x // x S }) → (hx : x + y = 0) → motive (_ : y, x + y = 0)) → motive x
Instances For
theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [] (S : ) :
theorem AddSubmonoid.fromLeftNeg_eq_iff {M : Type u_1} [] (S : ) (a : { x // }) (b : M) :
↑() = b a + b = 0
theorem Submonoid.fromLeftInv_eq_iff {M : Type u_1} [] (S : ) (a : { x // }) (b : M) :
↑() = b a * b = 1
theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [] (S : ) (x : { x // }) (y : { x // }) :
ZeroHom.toFun { toFun := , map_zero' := (_ : ) } (x + y) = ZeroHom.toFun { toFun := , map_zero' := (_ : ) } x + ZeroHom.toFun { toFun := , map_zero' := (_ : ) } y
noncomputable def AddSubmonoid.fromCommLeftNeg {M : Type u_1} [] (S : ) :
{ x // } →+ { x // x S }

The AddMonoidHom from S.leftNeg to S sending an element to its right additive inverse in S.

Instances For
theorem AddSubmonoid.fromCommLeftNeg.proof_1 {M : Type u_1} [] (S : ) :
@[simp]
theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [] (S : ) :
∀ (a : { x // }),
@[simp]
theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [] (S : ) :
∀ (a : { x // }),
noncomputable def Submonoid.fromCommLeftInv {M : Type u_1} [] (S : ) :
{ x // } →* { x // x S }

The MonoidHom from S.leftInv to S sending an element to its right inverse in S.

Instances For
noncomputable def AddSubmonoid.leftNegEquiv {M : Type u_1} [] (S : ) (hS : ) :
{ x // } ≃+ { x // x S }

The additive submonoid of pointwise additive inverse of S is AddEquiv to S.

Instances For
theorem AddSubmonoid.leftNegEquiv.proof_3 {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
(fun x => (fun x' hx => { val := x'.neg, property := (_ : y, x'.neg + y = 0) }) (Classical.choose (hS x (_ : x S))) (_ : ↑(Classical.choose (hS x (_ : x S))) = x)) () = x
theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [] (S : ) (x : { x // }) (y : { x // }) :
ZeroHom.toFun () (x + y) =
theorem AddSubmonoid.leftNegEquiv.proof_4 {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
ZeroHom.toFun () ((fun x => (fun x' hx => { val := x'.neg, property := (_ : y, x'.neg + y = 0) }) (Classical.choose (hS x (_ : x S))) (_ : ↑(Classical.choose (hS x (_ : x S))) = x)) x) = x
theorem AddSubmonoid.leftNegEquiv.proof_1 {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
theorem AddSubmonoid.leftNegEquiv.proof_2 {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
↑(Classical.choose (hS x (_ : x S))) = x
@[simp]
theorem AddSubmonoid.leftNegEquiv_apply {M : Type u_1} [] (S : ) (hS : ) :
∀ (a : { x // }), ↑() a =
@[simp]
theorem Submonoid.leftInvEquiv_apply {M : Type u_1} [] (S : ) (hS : ) :
∀ (a : { x // }), ↑() a =
noncomputable def Submonoid.leftInvEquiv {M : Type u_1} [] (S : ) (hS : ) :
{ x // } ≃* { x // x S }

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

Instances For
@[simp]
theorem AddSubmonoid.fromLeftNeg_leftNegEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
@[simp]
theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
Submonoid.fromLeftInv S (↑() x) = x
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_fromLeftNeg {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
↑() () = x
@[simp]
theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
↑() () = x
theorem AddSubmonoid.leftNegEquiv_add {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
↑(↑() x) + x = 0
theorem Submonoid.leftInvEquiv_mul {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
↑(↑() x) * x = 1
theorem AddSubmonoid.add_leftNegEquiv {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
x + ↑(↑() x) = 0
theorem Submonoid.mul_leftInvEquiv {M : Type u_1} [] (S : ) (hS : ) (x : { x // }) :
x * ↑(↑() x) = 1
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_add {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
↑(↑() x) + x = 0
@[simp]
theorem Submonoid.leftInvEquiv_symm_mul {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
↑(↑() x) * x = 1
@[simp]
theorem AddSubmonoid.add_leftNegEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
x + ↑(↑() x) = 0
@[simp]
theorem Submonoid.mul_leftInvEquiv_symm {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
x * ↑(↑() x) = 1
theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [] (S : ) :
theorem Submonoid.leftInv_eq_inv {M : Type u_1} [] (S : ) :
@[simp]
theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [] (S : ) (x : { x // }) :
↑() = -x
@[simp]
theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [] (S : ) (x : { x // }) :
↑() = (x)⁻¹
@[simp]
theorem AddSubmonoid.leftNegEquiv_symm_eq_neg {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
↑(↑() x) = -x
@[simp]
theorem Submonoid.leftInvEquiv_symm_eq_inv {M : Type u_1} [] (S : ) (hS : ) (x : { x // x S }) :
↑(↑() x) = (x)⁻¹