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.

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_1 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_10 {M : Type u_1} [AddMonoid M] : ∀ (n : ℕ) (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_7 {M : Type u_1} [AddMonoid M] : ∀ (a b : ↥(IsAddUnit.addSubmonoid M)), a - b = a - b

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_6 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : IsAddUnit ↑{ val := (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg, neg := ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)), val_neg := (_ : (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg + ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = 0), neg_val := (_ : ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) + (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg = 0) }

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_8 {M : Type u_1} [AddMonoid M] : ∀ (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec 0 a = zsmulRec 0 a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_9 {M : Type u_1} [AddMonoid M] : ∀ (n : ℕ) (a : ↥(IsAddUnit.addSubmonoid M)), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

noncomputable instance AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid {M : Type u_1} [AddMonoid M] : AddGroup ↥(IsAddUnit.addSubmonoid M)

Equations

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

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_5 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) + (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_2 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : IsAddUnit ↑(-IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M))

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg + ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_11 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : -x + x = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_3 {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑x ∈ IsAddUnit.addSubmonoid M

noncomputable instance Submonoid.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidSubmonoid {M : Type u_1} [Monoid M] : Group ↥(IsUnit.submonoid M)

Equations

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

theorem AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_1 {M : Type u_1} [AddCommMonoid M] (a : ↥(IsAddUnit.addSubmonoid M)) (b : ↥(IsAddUnit.addSubmonoid M)) : a + b = b + a

noncomputable instance AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid {M : Type u_1} [AddCommMonoid M] : AddCommGroup ↥(IsAddUnit.addSubmonoid M)

Equations

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

noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidSubmonoid {M : Type u_1} [CommMonoid M] : CommGroup ↥(IsUnit.submonoid M)

Equations

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

theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [AddMonoid M] (x : ↥(IsAddUnit.addSubmonoid M)) : ↑(-x) = ↑(-IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M))

theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [Monoid M] (x : ↥(IsUnit.submonoid M)) : ↑x⁻¹ = ↑(IsUnit.unit (_ : ↑x ∈ IsUnit.submonoid M))⁻¹

theorem AddSubmonoid.leftNeg.proof_2 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ∃ (y : ↥S), 0 + ↑y = 0

abbrev AddSubmonoid.leftNeg.match_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (_b : M) (motive : _b ∈ {x : M | ∃ (y : ↥S), x + ↑y = 0} → Prop) : ∀ (x : _b ∈ {x : M | ∃ (y : ↥S), x + ↑y = 0}), (∀ (b' : ↥S) (hb : _b + ↑b' = 0), motive (_ : ∃ (y : ↥S), _b + ↑y = 0)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {a : M} (_b : M) : a ∈ {x : M | ∃ (y : ↥S), x + ↑y = 0} → _b ∈ {x : M | ∃ (y : ↥S), x + ↑y = 0} → a + _b ∈ {x : M | ∃ (y : ↥S), x + ↑y = 0}

def AddSubmonoid.leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubmonoid M

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

Equations

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

def Submonoid.leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) : Submonoid M

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

Equations

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

theorem AddSubmonoid.leftNeg_leftNeg_le {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubmonoid.leftNeg (AddSubmonoid.leftNeg S) ≤ S

theorem Submonoid.leftInv_leftInv_le {M : Type u_1} [Monoid M] (S : Submonoid M) : Submonoid.leftInv (Submonoid.leftInv S) ≤ S

theorem AddSubmonoid.addUnit_mem_leftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : AddUnits M) (hx : ↑x ∈ S) : ↑(-x) ∈ AddSubmonoid.leftNeg S

theorem Submonoid.unit_mem_leftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : Mˣ) (hx : ↑x ∈ S) : ↑x⁻¹ ∈ Submonoid.leftInv S

theorem AddSubmonoid.leftNeg_leftNeg_eq {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) : AddSubmonoid.leftNeg (AddSubmonoid.leftNeg S) = S

theorem Submonoid.leftInv_leftInv_eq {M : Type u_1} [Monoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) : Submonoid.leftInv (Submonoid.leftInv S) = S

noncomputable def AddSubmonoid.fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : ↥(AddSubmonoid.leftNeg S) → ↥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.

Equations

• AddSubmonoid.fromLeftNeg S x = Exists.choose (_ : ↑x ∈ AddSubmonoid.leftNeg S)

theorem AddSubmonoid.fromLeftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑x ∈ AddSubmonoid.leftNeg S

noncomputable def Submonoid.fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) : ↥(Submonoid.leftInv S) → ↥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.

Equations

• Submonoid.fromLeftInv S x = Exists.choose (_ : ↑x ∈ Submonoid.leftInv S)

@[simp]

theorem AddSubmonoid.add_fromLeftNeg {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑x + ↑(AddSubmonoid.fromLeftNeg S x) = 0

@[simp]

theorem Submonoid.mul_fromLeftInv {M : Type u_1} [Monoid M] (S : Submonoid M) (x : ↥(Submonoid.leftInv S)) : ↑x * ↑(Submonoid.fromLeftInv S x) = 1

@[simp]

theorem AddSubmonoid.fromLeftNeg_zero {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) : AddSubmonoid.fromLeftNeg S 0 = 0

@[simp]

theorem Submonoid.fromLeftInv_one {M : Type u_1} [Monoid M] (S : Submonoid M) : Submonoid.fromLeftInv S 1 = 1

@[simp]

theorem AddSubmonoid.fromLeftNeg_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑(AddSubmonoid.fromLeftNeg S x) + ↑x = 0

@[simp]

theorem Submonoid.fromLeftInv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (x : ↥(Submonoid.leftInv S)) : ↑(Submonoid.fromLeftInv S x) * ↑x = 1

abbrev AddSubmonoid.leftNeg_le_isAddUnit.match_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : M) (motive : x ∈ AddSubmonoid.leftNeg S → Prop) : ∀ (x_1 : x ∈ AddSubmonoid.leftNeg S), (∀ (y : ↥S) (hx : x + ↑y = 0), motive (_ : ∃ (y : ↥S), x + ↑y = 0)) → motive x_1

Equations

• (_ : motive x) = (_ : motive x)

theorem AddSubmonoid.leftNeg_le_isAddUnit {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : AddSubmonoid.leftNeg S ≤ IsAddUnit.addSubmonoid M

theorem Submonoid.leftInv_le_isUnit {M : Type u_1} [CommMonoid M] (S : Submonoid M) : Submonoid.leftInv S ≤ IsUnit.submonoid M

theorem AddSubmonoid.fromLeftNeg_eq_iff {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (a : ↥(AddSubmonoid.leftNeg S)) (b : M) : ↑(AddSubmonoid.fromLeftNeg S a) = b ↔ ↑a + b = 0

theorem Submonoid.fromLeftInv_eq_iff {M : Type u_1} [CommMonoid M] (S : Submonoid M) (a : ↥(Submonoid.leftInv S)) (b : M) : ↑(Submonoid.fromLeftInv S a) = b ↔ ↑a * b = 1

theorem AddSubmonoid.fromCommLeftNeg.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : AddSubmonoid.fromLeftNeg S 0 = 0

theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) (y : ↥(AddSubmonoid.leftNeg S)) : { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) }.toFun (x + y) = { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) }.toFun x + { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) }.toFun y

noncomputable def AddSubmonoid.fromCommLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ↥(AddSubmonoid.leftNeg S) →+ ↥S

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

Equations

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

@[simp]

theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) : ∀ (a : ↥(AddSubmonoid.leftNeg S)), (AddSubmonoid.fromCommLeftNeg S) a = AddSubmonoid.fromLeftNeg S a

@[simp]

theorem Submonoid.fromCommLeftInv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) : ∀ (a : ↥(Submonoid.leftInv S)), (Submonoid.fromCommLeftInv S) a = Submonoid.fromLeftInv S a

noncomputable def Submonoid.fromCommLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) : ↥(Submonoid.leftInv S) →* ↥S

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

Equations

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

noncomputable def AddSubmonoid.leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) : ↥(AddSubmonoid.leftNeg S) ≃+ ↥S

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

Equations

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

theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) (y : ↥(AddSubmonoid.leftNeg S)) : (↑(AddSubmonoid.fromCommLeftNeg S)).toFun (x + y) = (↑(AddSubmonoid.fromCommLeftNeg S)).toFun x + (↑(AddSubmonoid.fromCommLeftNeg S)).toFun y

theorem AddSubmonoid.leftNegEquiv.proof_1 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : ↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.leftNegEquiv.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : ↑(Classical.choose (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = ↑x

theorem AddSubmonoid.leftNegEquiv.proof_3 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : (fun (x : ↥S) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => { val := x'.neg, property := (_ : ∃ (y : ↥S), x'.neg + ↑y = 0) }) (Classical.choose (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) (_ : ↑(Classical.choose (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = ↑x)) ((↑(AddSubmonoid.fromCommLeftNeg S)).toFun x) = x

theorem AddSubmonoid.leftNegEquiv.proof_4 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : (↑(AddSubmonoid.fromCommLeftNeg S)).toFun ((fun (x : ↥S) => (fun (x' : AddUnits M) (hx : ↑x' = ↑x) => { val := x'.neg, property := (_ : ∃ (y : ↥S), x'.neg + ↑y = 0) }) (Classical.choose (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) (_ : ↑(Classical.choose (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = ↑x)) x) = x

@[simp]

theorem AddSubmonoid.leftNegEquiv_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) : ∀ (a : ↥(AddSubmonoid.leftNeg S)), (AddSubmonoid.leftNegEquiv S hS) a = (↑(AddSubmonoid.fromCommLeftNeg S)).toFun a

@[simp]

theorem Submonoid.leftInvEquiv_apply {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) : ∀ (a : ↥(Submonoid.leftInv S)), (Submonoid.leftInvEquiv S hS) a = (↑(Submonoid.fromCommLeftInv S)).toFun a

noncomputable def Submonoid.leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) : ↥(Submonoid.leftInv S) ≃* ↥S

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

Equations

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

@[simp]

theorem AddSubmonoid.fromLeftNeg_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : AddSubmonoid.fromLeftNeg S ((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) = x

@[simp]

theorem Submonoid.fromLeftInv_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) : Submonoid.fromLeftInv S ((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = x

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_fromLeftNeg {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : (AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) (AddSubmonoid.fromLeftNeg S x) = x

@[simp]

theorem Submonoid.leftInvEquiv_symm_fromLeftInv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥(Submonoid.leftInv S)) : (MulEquiv.symm (Submonoid.leftInvEquiv S hS)) (Submonoid.fromLeftInv S x) = x

theorem AddSubmonoid.leftNegEquiv_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑((AddSubmonoid.leftNegEquiv S hS) x) + ↑x = 0

theorem Submonoid.leftInvEquiv_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥(Submonoid.leftInv S)) : ↑((Submonoid.leftInvEquiv S hS) x) * ↑x = 1

theorem AddSubmonoid.add_leftNegEquiv {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑x + ↑((AddSubmonoid.leftNegEquiv S hS) x) = 0

theorem Submonoid.mul_leftInvEquiv {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥(Submonoid.leftInv S)) : ↑x * ↑((Submonoid.leftInvEquiv S hS) x) = 1

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_add {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : ↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) + ↑x = 0

@[simp]

theorem Submonoid.leftInvEquiv_symm_mul {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) : ↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) * ↑x = 1

@[simp]

theorem AddSubmonoid.add_leftNegEquiv_symm {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : ↑x + ↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) = 0

@[simp]

theorem Submonoid.mul_leftInvEquiv_symm {M : Type u_1} [CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) : ↑x * ↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = 1

theorem AddSubmonoid.leftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) : AddSubmonoid.leftNeg S = -S

theorem Submonoid.leftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) : Submonoid.leftInv S = S⁻¹

@[simp]

theorem AddSubmonoid.fromLeftNeg_eq_neg {M : Type u_1} [AddGroup M] (S : AddSubmonoid M) (x : ↥(AddSubmonoid.leftNeg S)) : ↑(AddSubmonoid.fromLeftNeg S x) = -↑x

@[simp]

theorem Submonoid.fromLeftInv_eq_inv {M : Type u_1} [Group M] (S : Submonoid M) (x : ↥(Submonoid.leftInv S)) : ↑(Submonoid.fromLeftInv S x) = (↑x)⁻¹

@[simp]

theorem AddSubmonoid.leftNegEquiv_symm_eq_neg {M : Type u_1} [AddCommGroup M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : ↥S) : ↑((AddEquiv.symm (AddSubmonoid.leftNegEquiv S hS)) x) = -↑x

@[simp]

theorem Submonoid.leftInvEquiv_symm_eq_inv {M : Type u_1} [CommGroup M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S) : ↑((MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = (↑x)⁻¹