Equiv.addLeft_symm_apply
theorem Equiv.addLeft_symm_apply :
∀ {G : Type u_10} [inst : AddGroup G] (a : G), ⇑(Equiv.addLeft a).symm = fun x => -a + x
This theorem states that for any addable group `G` and any element `a` in `G`, the inverse of the function that adds `a` to the left of another element in `G` is equivalent to the function that subtracts `a` from its argument. In other words, if you have an addition operation that initially adds `a` to some element, undoing that operation is equivalent to subtracting `a` from that element. This theorem is especially useful for simplification processes within Lean, but it's not used by the `simp` tactic.
More concisely: For any additive group (G, +) and element a in G, the function x ↔ x + a is equivalent to the function x ↔ x - a.
|
Equiv.mulRight_symm_apply
theorem Equiv.mulRight_symm_apply :
∀ {G : Type u_10} [inst : Group G] (a : G), ⇑(Equiv.mulRight a).symm = fun x => x * a⁻¹
This theorem states that for any group `G` and any element `a` in `G`, the inverse of the permutation generated by right multiplication by `a` is equivalent to a function that right multiplies an element `x` in `G` by the inverse of `a`. In other words, if you first multiply by `a` on the right and then by `a⁻¹` on the right, it's the same as doing nothing, which is a characteristic property of the inverse in a group.
More concisely: For any group `G` and element `a` in `G`, the right multiplication by `a` and its inverse is equivalent: `a * x * a⁻¹ ≡ x` for all `x` in `G`.
|
Equiv.addRight_symm
theorem Equiv.addRight_symm :
∀ {G : Type u_10} [inst : AddGroup G] (a : G), (Equiv.addRight a).symm = Equiv.addRight (-a)
The theorem `Equiv.addRight_symm` states that for any type `G` that forms an additive group, for every element `a` of `G`, the inverse of the permutation resulting from right addition by `a` is the same as the permutation resulting from right addition by `-a`. In other words, adding `a` to the right and then adding `-a` to the right is equivalent to doing nothing, demonstrating the symmetry of right addition in an additive group.
More concisely: For any additive group G and element a in G, the right addition by a and then by -a is equal to the identity permutation on G.
|
Equiv.addRight_symm_apply
theorem Equiv.addRight_symm_apply :
∀ {G : Type u_10} [inst : AddGroup G] (a : G), ⇑(Equiv.addRight a).symm = fun x => x + -a
This theorem states that for any given type `G` that forms an `AddGroup`, the inverse function of the permutation associated with right addition by an element `a` of `G` is equivalent to the function that adds the additive inverse of `a` to its input. In the context of group theory, this means that 'undoing' a right addition of an element in a group is the same as adding the negative of that element.
More concisely: For any additive group `G` and element `a` in `G`, the inverse permutation of right multiplication by `a` is equivalent to left addition of `-a`.
|
Equiv.mulLeft_symm_apply
theorem Equiv.mulLeft_symm_apply :
∀ {G : Type u_10} [inst : Group G] (a : G), ⇑(Equiv.mulLeft a).symm = fun x => a⁻¹ * x
This theorem states that for any group `G` and any element `a` in `G`, applying the inverse of the function `Equiv.mulLeft a` (which is a function that performs left multiplication by `a`) to an element `x` in `G` is equivalent to multiplying the inverse of `a` on the left by `x`. In other words, the inverse function of left multiplication by `a` is the function that multiplies the inverse of `a` on the left.
More concisely: For any group `G` and its element `a`, the function `Equiv.mulLeft a.symm` (inverse of left multiplication by `a`) equals left multiplication by `a.inv` (inverse of `a`).
|