Submonoid.mul_fromLeftInv
theorem Submonoid.mul_fromLeftInv :
∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M) (x : ↥S.leftInv), ↑x * ↑(S.fromLeftInv x) = 1
The theorem `Submonoid.mul_fromLeftInv` states that for any type `M` that forms a monoid, and for any submonoid `S` of `M`, and for any element `x` from the submonoid of `S` that consists of left inverses of elements in `S`, the product of `x` and the element of `S` that is the right inverse of `x` (obtained through the function `Submonoid.fromLeftInv`) is equal to the identity (`1`) of the monoid. In mathematical terms, for any $x$ in the set of left inverses of a submonoid $S$, we have $x*(x^{-1}) = 1$, where $x^{-1}$ is the right inverse of $x$ in $S$.
More concisely: For any submonoid `S` of a monoid `M` and any element `x` in `S` with right inverse `x⁻¹`, we have `x * x⁻¹ = 1`.
|
AddSubmonoid.add_fromLeftNeg
theorem AddSubmonoid.add_fromLeftNeg :
∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M) (x : ↥S.leftNeg), ↑x + ↑(S.fromLeftNeg x) = 0
The theorem `AddSubmonoid.add_fromLeftNeg` states that for any type `M` which has an addition operation (`AddMonoid M`), for any additive submonoid `S` of `M`, and for any element `x` in the set of left additive inverses of `S` (denoted by `AddSubmonoid.leftNeg S`), the sum of `x` and its right additive inverse in `S` (obtained using the function `AddSubmonoid.fromLeftNeg`) is zero. In other words, the theorem establishes that every element in the left additive inverses of `S` and its corresponding right additive inverse in `S` sum up to zero.
More concisely: For any additive submonoid `S` of an additive monoid `M`, and for any `x` in the set of left additive inverses of `S`, the element `x` and its right additive inverse in `S` sum up to zero.
|