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.

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_12 {M : Type u_1} [AddMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) :

a + 0 = a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_14 {M : Type u_1} [AddMonoid M] (n : ℕ) (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

(fun n x => n • x) (n + 1) x = x + (fun n x => n • x) n x

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

0 + a = a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_23 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

-x + x = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_6 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

IsAddUnit ↑(-IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M))

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_8 {M : Type u_1} [AddMonoid M] :

↑0 = ↑0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_19 {M : Type u_1} [AddMonoid M] :

∀ (a b : { x // x ∈ IsAddUnit.addSubmonoid M }), a - b = a - b

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_15 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_9 {M : Type u_1} [AddMonoid M] :

∀ (x x_1 : { x // x ∈ IsAddUnit.addSubmonoid M }), ↑(x + x_1) = ↑(x + x_1)

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_22 {M : Type u_1} [AddMonoid M] :

∀ (n : ℕ) (a : { x // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec (Int.negSucc n) a = zsmulRec (Int.negSucc n) a

noncomputable instance AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid {M : Type u_1} [AddMonoid M] :

AddGroup { x // x ∈ IsAddUnit.addSubmonoid M }

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_16 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg + ↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_10 {M : Type u_1} [AddMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) (b : { x // x ∈ IsAddUnit.addSubmonoid M }) (c : { x // x ∈ IsAddUnit.addSubmonoid M }) :

a + b + c = a + (b + c)

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_2 {M : Type u_1} [AddMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) :

a + 0 = a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_21 {M : Type u_1} [AddMonoid M] :

∀ (n : ℕ) (a : { x // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec (Int.ofNat (Nat.succ n)) a = zsmulRec (Int.ofNat (Nat.succ n)) a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_17 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

↑(IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)) + (IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M)).neg = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_7 {M : Type u_1} [AddMonoid M] :

Function.Injective fun a => ↑a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_13 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

(fun n x => n • x) 0 x = 0

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_18 {M : Type u_1} [AddMonoid M] (x : { x // 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_20 {M : Type u_1} [AddMonoid M] :

∀ (a : { x // x ∈ IsAddUnit.addSubmonoid M }), zsmulRec 0 a = zsmulRec 0 a

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_4 {M : Type u_1} [AddMonoid M] (n : ℕ) (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

AddMonoid.nsmul (n + 1) x = x + AddMonoid.nsmul n x

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_5 {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

↑x ∈ IsAddUnit.addSubmonoid M

theorem AddSubmonoid.instAddGroupSubtypeMemAddSubmonoidToAddZeroClassInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_11 {M : Type u_1} [AddMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) :

0 + a = a

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

AddMonoid.nsmul 0 x = 0

noncomputable instance Submonoid.instGroupSubtypeMemSubmonoidToMulOneClassInstMembershipInstSetLikeSubmonoidSubmonoid {M : Type u_1} [Monoid M] :

Group { x // x ∈ IsUnit.submonoid M }

theorem AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_2 {M : Type u_1} [AddCommMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) (b : { x // x ∈ IsAddUnit.addSubmonoid M }) :

a + b = b + a

theorem AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid.proof_1 {M : Type u_1} [AddCommMonoid M] (a : { x // x ∈ IsAddUnit.addSubmonoid M }) :

-a + a = 0

noncomputable instance AddSubmonoid.instAddCommGroupSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidAddSubmonoid {M : Type u_1} [AddCommMonoid M] :

AddCommGroup { x // x ∈ IsAddUnit.addSubmonoid M }

noncomputable instance Submonoid.instCommGroupSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidSubmonoid {M : Type u_1} [CommMonoid M] :

CommGroup { x // x ∈ IsUnit.submonoid M }

theorem AddSubmonoid.IsUnit.Submonoid.coe_neg {M : Type u_1} [AddMonoid M] (x : { x // x ∈ IsAddUnit.addSubmonoid M }) :

↑(-x) = ↑(-IsAddUnit.addUnit (_ : ↑x ∈ IsAddUnit.addSubmonoid M))

theorem Submonoid.IsUnit.Submonoid.coe_inv {M : Type u_1} [Monoid M] (x : { x // x ∈ IsUnit.submonoid M }) :

↑x⁻¹ = ↑(IsUnit.unit (_ : ↑x ∈ IsUnit.submonoid M))⁻¹

theorem AddSubmonoid.leftNeg.proof_1 {M : Type u_1} [AddMonoid M] (S : AddSubmonoid M) {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} [AddMonoid M] (S : AddSubmonoid M) :

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} [AddMonoid M] (S : AddSubmonoid M) (_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} [AddMonoid M] (S : AddSubmonoid M) :

∃ y, 0 + ↑y = 0

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

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

Instances For

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

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

↑x ∈ AddSubmonoid.leftNeg S

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

{ x // x ∈ AddSubmonoid.leftNeg S } → { 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} [Monoid M] (S : Submonoid M) :

{ x // x ∈ Submonoid.leftInv S } → { 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} [AddMonoid M] (S : AddSubmonoid M) (x : { x // 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 : { x // 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 : { x // 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 : { x // x ∈ Submonoid.leftInv S }) :

↑(Submonoid.fromLeftInv S x) * ↑x = 1

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

AddSubmonoid.leftNeg S ≤ IsAddUnit.addSubmonoid M

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 : x ∈ AddSubmonoid.leftNeg S) → ((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} [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 : { x // x ∈ 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 : { x // x ∈ Submonoid.leftInv S }) (b : M) :

↑(Submonoid.fromLeftInv S a) = b ↔ ↑a * b = 1

theorem AddSubmonoid.fromCommLeftNeg.proof_2 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : { x // x ∈ AddSubmonoid.leftNeg S }) (y : { x // x ∈ AddSubmonoid.leftNeg S }) :

ZeroHom.toFun { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) } (x + y) = ZeroHom.toFun { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) } x + ZeroHom.toFun { toFun := AddSubmonoid.fromLeftNeg S, map_zero' := (_ : AddSubmonoid.fromLeftNeg S 0 = 0) } y

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

{ x // x ∈ AddSubmonoid.leftNeg S } →+ { 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} [AddCommMonoid M] (S : AddSubmonoid M) :

AddSubmonoid.fromLeftNeg S 0 = 0

@[simp]

theorem AddSubmonoid.fromCommLeftNeg_apply {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) :

∀ (a : { x // x ∈ 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 : { x // x ∈ Submonoid.leftInv S }), ↑(Submonoid.fromCommLeftInv S) a = Submonoid.fromLeftInv S a

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

{ x // x ∈ Submonoid.leftInv S } →* { 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} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) :

{ x // x ∈ AddSubmonoid.leftNeg S } ≃+ { 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} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x // x ∈ AddSubmonoid.leftNeg S }) :

(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)) (ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) x) = x

theorem AddSubmonoid.leftNegEquiv.proof_5 {M : Type u_1} [AddCommMonoid M] (S : AddSubmonoid M) (x : { x // x ∈ AddSubmonoid.leftNeg S }) (y : { x // x ∈ AddSubmonoid.leftNeg S }) :

ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) (x + y) = ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) x + ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) y

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

ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) ((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} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x // 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 : { x // x ∈ S }) :

↑(Classical.choose (hS ↑x (_ : ↑x ∈ S))) = ↑x

@[simp]

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

∀ (a : { x // x ∈ AddSubmonoid.leftNeg S }), ↑(AddSubmonoid.leftNegEquiv S hS) a = ZeroHom.toFun (↑(AddSubmonoid.fromCommLeftNeg S)) a

@[simp]

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

∀ (a : { x // x ∈ Submonoid.leftInv S }), ↑(Submonoid.leftInvEquiv S hS) a = OneHom.toFun (↑(Submonoid.fromCommLeftInv S)) a

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

{ x // x ∈ Submonoid.leftInv S } ≃* { 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} [AddCommMonoid M] (S : AddSubmonoid M) (hS : S ≤ IsAddUnit.addSubmonoid M) (x : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // 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 : { x // x ∈ S }) :

↑(↑(MulEquiv.symm (Submonoid.leftInvEquiv S hS)) x) = (↑x)⁻¹