MulEquiv.symm_map_mul
theorem MulEquiv.symm_map_mul :
∀ {M : Type u_12} {N : Type u_13} [inst : Mul M] [inst_1 : Mul N] (h : M ≃* N) (x y : N),
h.symm (x * y) = h.symm x * h.symm y
The theorem `MulEquiv.symm_map_mul` states that for any two types `M` and `N` that have multiplication operations, given a multiplicative equivalence `h` between `M` and `N`, and two elements `x` and `y` from `N`, the image of the multiplication of `x` and `y` under the inverse of `h` is equal to the multiplication of the images of `x` and `y` under the inverse of `h`. In mathematical terms, it says that the inverse of a multiplicative equivalence preserves multiplication.
More concisely: Let `h` be a multiplicative equivalence between types `M` and `N`. Then for all `x, y ∈ N`, we have `h⁻¹(x * y) = h⁻¹(x) * h⁻¹(y)`.
|
AddEquiv.map_add
theorem AddEquiv.map_add :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N) (x y : M), f (x + y) = f x + f y := by
sorry
This theorem states that an additive isomorphism, denoted as `f : M ≃+ N`, preserves addition. Specifically, for any two elements `x` and `y` from the type `M` equipped with addition operation, the image of the sum under the isomorphism is equal to the sum of the images, i.e., `f (x + y) = f x + f y`. In other words, applying `f` to the sum of `x` and `y` is the same as adding the images of `x` and `y` under `f`. This property is a key characteristic of additive isomorphisms.
More concisely: An additive isomorphism preserves addition, that is, for all `x, y` in `M`, `f (x + y) = f x + f y`.
|
AddEquiv.map_add'
theorem AddEquiv.map_add' :
∀ {A : Type u_12} {B : Type u_13} [inst : Add A] [inst_1 : Add B] (self : A ≃+ B) (x y : A),
self.toFun (x + y) = self.toFun x + self.toFun y
This theorem, `AddEquiv.map_add'`, states that for any two types `A` and `B` that have addition defined on them, if there exists an additive equivalence (denoted as `A ≃+ B`) between `A` and `B`, then this equivalence preserves addition. In other words, for any elements `x` and `y` in `A`, applying the equivalence to the sum of `x` and `y` (i.e., `x + y`) is the same as applying the equivalence to `x` and `y` separately and then adding the results.
More concisely: Given types `A` and `B` with addition and an additive equivalence `A ≃+ B`, for all `x, y ∈ A`, `(x ≃+ y) + (x' ≃+ y') ≡ x + y ≃+ x' + y'`.
|
AddEquiv.map_eq_zero_iff
theorem AddEquiv.map_eq_zero_iff :
∀ {M : Type u_6} {N : Type u_7} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N) {x : M},
h x = 0 ↔ x = 0
This theorem states that for any two types `M` and `N` that have addition with zero (`AddZeroClass`), if there exists an additive equivalence (`h : M ≃+ N`) between `M` and `N`, then an element `x` of type `M` maps to zero under this equivalence if and only if `x` itself is zero. In other words, this theorem ensures that an additive equivalence preserves the property of being zero.
More concisely: For any types `M` and `N` with additive structures and an additive equivalence `h : M ≃+ N`, if `x : M` maps to zero in `N` under `h`, then `x` is zero in `M`.
|
AddEquivClass.map_add
theorem AddEquivClass.map_add :
∀ {F : Type u_12} {A : outParam (Type u_13)} {B : outParam (Type u_14)} [inst : Add A] [inst_1 : Add B]
[inst_2 : EquivLike F A B] [self : AddEquivClass F A B] (f : F) (a b : A), f (a + b) = f a + f b
This theorem, titled `map_add`, states that for any types `F`, `A`, and `B`, where `A` and `B` have addition defined on them, and for any equivalence-like relationship `EquivLike` between `A` and `B` represented by `F`, if `F` is an additive equivalence class (`AddEquivClass`), then the function `f` of type `F` preserves the operation of addition. More specifically, for any elements `a` and `b` of type `A`, adding `a` and `b` first and then applying `f` is the same as applying `f` to `a` and `b` separately and then adding the results. This property is fundamental to the concept of homomorphisms in abstract algebra.
More concisely: For any additive equivalence class `F` with respect to an equivalence-like relation between types `A` and `B` with additions defined, the function `f` of type `F` is a homomorphism, i.e., `f (x + y) = f x + f y` for all `x, y` in `A`.
|
MulEquiv.symm_apply_apply
theorem MulEquiv.symm_apply_apply :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (x : M), e.symm (e x) = x
The theorem `MulEquiv.symm_apply_apply` states that for any given multiplicative isomorphism `e` between two types `M` and `N`, both equipped with a multiplication operation, the inverse of `e` (`e.symm`) is a left inverse of `e`. Mathematically, for any element `x` in `M`, if we apply `e` to `x` and then apply `e.symm` to the result, we obtain `x` back. The statement can be written as: `e.symm (e x) = x`.
More concisely: For any multiplicative isomorphism `e` between types `M` and `N` with multiplication operations, `e.symm (e x) = x` for all `x` in `M`.
|
MulEquiv.map_mul'
theorem MulEquiv.map_mul' :
∀ {M : Type u_12} {N : Type u_13} [inst : Mul M] [inst_1 : Mul N] (self : M ≃* N) (x y : M),
self.toFun (x * y) = self.toFun x * self.toFun y
This theorem states that for any two types `M` and `N` that have multiplication (`Mul M` and `Mul N`), if there is a multiplicative equivalence (`M ≃* N`) between them (denoted as `self`), this equivalence preserves multiplication. That is, if you apply the function represented by this equivalence to the product of two elements in `M` (`x * y`), it's the same as applying the function to each element and then taking the product in `N` (`self.toFun x * self.toFun y`). This kind of property is essential for the concept of a homomorphism in abstract algebra.
More concisely: Given types `M` and `N` with multiplication and a multiplicative equivalence `self : M ≃* N`, the image of the product of two elements in `M` under `self` is equal to the product of their images in `N`. In other words, `self.toFun (x * y) = self.toFun x * self.toFun y` for all `x, y` in `M`.
|
MulEquiv.surjective
theorem MulEquiv.surjective :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Surjective ⇑e
The theorem `MulEquiv.surjective` states that for all types `M` and `N` equipped with multiplication (`Mul M` and `Mul N`), every multiplicative equivalence `e` from `M` to `N` is surjective. In other words, for every element `n` of `N`, there exists an element `m` of `M` such that applying the equivalence `e` to `m` results in `n`. This means that the equivalence `e` maps every element of `M` onto some element of `N`, covering the entirety of `N`.
More concisely: Given types `M` and `N` with multiplications, every multiplicative equivalence from `M` to `N` is a surjection.
|
MulEquiv.map_div
theorem MulEquiv.map_div :
∀ {G : Type u_10} {H : Type u_11} [inst : Group G] [inst_1 : DivisionMonoid H] (h : G ≃* H) (x y : G),
h (x / y) = h x / h y
This theorem states that a multiplicative equivalence of groups preserves the operation of division. In other words, for any two elements `x` and `y` of a group `G` that is multiplicatively equivalent to a division monoid `H`, the image of the division of `x` by `y` under this equivalence is the same as the division of the images of `x` and `y` under the same equivalence.
More concisely: If `G` is a group multiplicatively equivalent to a division monoid `H`, then for all `x` and `y` in `G`, `x / y = (x') / (y')` holds in `G` if and only if `x' = z * x` and `y' = z * y` hold in `G` for some `z` in `G`, where `x'` and `y'` are the images of `x` and `y` under the equivalence.
|
AddEquiv.map_neg
theorem AddEquiv.map_neg :
∀ {G : Type u_10} {H : Type u_11} [inst : AddGroup G] [inst_1 : SubtractionMonoid H] (h : G ≃+ H) (x : G),
h (-x) = -h x
This theorem states that for any two types `G` and `H`, where `G` is an additive group and `H` is a subtraction monoid, any additive equivalence `h` from `G` to `H` preserves the negation operation. In other words, applying `h` to the negation of an element `x` from `G` gives the same result as negating the result of applying `h` to `x`. This is symbolically written as `h (-x) = -h x`.
More concisely: For any additive group homomorphism `h` from type `G` to a subtraction monoid `H`, `h` preserves negation, i.e., `h (-x) = -h x` for all `x` in `G`.
|
MulEquiv.map_one
theorem MulEquiv.map_one :
∀ {M : Type u_6} {N : Type u_7} [inst : MulOneClass M] [inst_1 : MulOneClass N] (h : M ≃* N), h 1 = 1
This theorem states that for all multiplicative isomorphisms between two monoids (which are structures equipped with an associative multiplication operation and an identity element), the identity element (denoted by `1`) of the first monoid is mapped to the identity element of the second monoid. Therefore, a multiplicative isomorphism preserves the identity element in a monoid structure.
More concisely: Given two monoids with multiplicative isomorphisms between them, the identity elements are mapped to each other under the isomorphisms.
|
MulEquiv.ext
theorem MulEquiv.ext :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] {f g : M ≃* N}, (∀ (x : M), f x = g x) → f = g := by
sorry
This theorem states that two multiplicative isomorphisms `f` and `g` between two types `M` and `N` (which both have multiplication operations) are equal if they are defined by the same underlying function. In other words, if for all elements `x` of type `M`, applying `f` to `x` yields the same result as applying `g` to `x`, then `f` and `g` are the same multiplicative isomorphism.
More concisely: If two multiplicative isomorphisms between types with multiplication operations have the same function representation, then they are equal.
|
MulEquiv.apply_symm_apply
theorem MulEquiv.apply_symm_apply :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (y : N), e (e.symm y) = y
This theorem states that for any two types `M` and `N` equipped with a multiplication operation (denoted `Mul M` and `Mul N` respectively), if there is a multiplicative isomorphism `e` between them (denoted `M ≃* N`), then the inverse of this isomorphism, `e.symm`, applied to any element `y` of `N`, and then re-applied `e` to the result, returns `y` itself. In other words, `e.symm` is a right inverse of `e`. This can be formally written as `e (e.symm y) = y` for any `y` in `N`.
More concisely: Given types `M` and `N` with multiplicative structures and a multiplicative isomorphism `e : M ≃* N`, the inverse `e.symm` is a right inverse of `e`, i.e., `e (e.symm y) = y` for any `y` in `N`.
|
AddEquiv.injective
theorem AddEquiv.injective :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Injective ⇑e
This theorem states that for any two types `M` and `N` which are equipped with addition operations (symbolized by `[inst : Add M]` and `[inst_1 : Add N]`), any additive equivalence `e` between `M` and `N` (`e : M ≃+ N`) is an injective function. In other words, if `e` maps two elements of `M` to the same element of `N` (i.e., `e(x) = e(y)`), then those two elements were actually the same (`x = y`). This property is fundamental to the concept of an additive equivalence, which should not only preserve the structure of addition but also retain distinctness of elements.
More concisely: Given types `M` and `N` with additions and an additive equivalence `e : M ≃+ N`, if `e(x) = e(y)` then `x = y`.
|
AddEquiv.map_sub
theorem AddEquiv.map_sub :
∀ {G : Type u_10} {H : Type u_11} [inst : AddGroup G] [inst_1 : SubtractionMonoid H] (h : G ≃+ H) (x y : G),
h (x - y) = h x - h y
This theorem states that an additive equivalence between two additive groups preserves the operation of subtraction. More specifically, for any two elements 'x' and 'y' of an additive group 'G', and a given additive equivalence 'h' mapping this group to another additive group 'H', the image of the difference between 'x' and 'y' under 'h' is equal to the difference between the images of 'x' and 'y' under 'h'. In mathematical terms, if 'G' and 'H' are additive groups and 'h' is an additive equivalence from 'G' to 'H', then for all 'x', 'y' in 'G', we have 'h(x - y) = h(x) - h(y)'.
More concisely: An additive equivalence between two additive groups preserves the operation of subtraction, that is, for all elements 'x' and 'y' in an additive group 'G' and an additive equivalence 'h' from 'G' to another additive group 'H', we have 'h(x - y) = h(x) - h(y)'.
|
AddEquiv.map_zero
theorem AddEquiv.map_zero :
∀ {M : Type u_6} {N : Type u_7} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N), h 0 = 0
This theorem states that an additive isomorphism of additive monoids maps the identity element (zero) in the source monoid to the identity element (zero) in the target monoid. In other words, if we have two additive monoids (types `M` and `N` with respective zero property classes), then for any additive isomorphism `h` from `M` to `N`, applying `h` to zero in `M` will always yield zero in `N`.
More concisely: Given additive monoids M and N and an additive isomorphism h from M to N, h(0\_M) = 0\_N.
|
AddEquiv.symm_apply_eq
theorem AddEquiv.symm_apply_eq :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x : N} {y : M},
e.symm x = y ↔ x = e y
The theorem `AddEquiv.symm_apply_eq` states that for any types `M` and `N` that have an addition operation, given an additive isomorphism `e` from `M` to `N`, and any elements `x` of `N` and `y` of `M`, the inverse isomorphism of `e` applied to `x` being equal to `y` is equivalent to `x` being equal to the forward isomorphism `e` applied to `y`. In other words, if we map `y` from `M` to `N` via `e` and get `x`, then mapping `x` back to `M` via the inverse of `e` will get us `y` again. This theorem captures the idea that an isomorphism and its inverse undo each other.
More concisely: Given additive types M and N with an additive isomorphism e between them, the inverse of e applied to x in N equals y in M if and only if e applied to y in M equals x in N.
|
AddEquiv.apply_eq_iff_eq
theorem AddEquiv.apply_eq_iff_eq :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) {x y : M}, e x = e y ↔ x = y := by
sorry
This theorem states that for any two types `M` and `N` that are equipped with an addition operation (denoted by `Add M` and `Add N`), given an additive equivalence `e` between `M` and `N` (denoted by `e : M ≃+ N`), for any two elements `x` and `y` of `M`, `x` is equal to `y` if and only if their images under `e` are equal. Essentially, this theorem shows that the given additive equivalence `e` preserves the equality of elements.
More concisely: For any additive equivalences `e : M ≃+ N` between types `M` and `N` equipped with addition operations, `x = y` in `M` if and only if `e x = e y` in `N`.
|
AddEquiv.surjective
theorem AddEquiv.surjective :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), Function.Surjective ⇑e
The theorem `AddEquiv.surjective` states that for any two types `M` and `N` which have addition (`Add`) defined on them, any additive equivalence (`AddEquiv`) `e` from `M` to `N` is a surjective function. In other words, for every element `n` in `N`, there exists an element `m` in `M` such that applying the additive equivalence `e` to `m` yields `n`.
More concisely: Given types `M` and `N` with addition and an additive equivalence `e` between them, `e` is a surjective function.
|
MulEquivClass.map_mul
theorem MulEquivClass.map_mul :
∀ {F : Type u_12} {A : outParam (Type u_13)} {B : outParam (Type u_14)} [inst : Mul A] [inst_1 : Mul B]
[inst_2 : EquivLike F A B] [self : MulEquivClass F A B] (f : F) (a b : A), f (a * b) = f a * f b
The theorem `MulEquivClass.map_mul` states that for any types `F`, `A`, and `B`, given multiplication operations on `A` and `B`, an equivalence relation between `A` and `B`, and `f` as a member of the `MulEquivClass` from `A` to `B`, the function `f` preserves multiplication. In other words, if you multiply two elements `a` and `b` of `A`, and then apply `f`, the result is the same as if you first applied `f` to `a` and `b` separately and then multiplied the results in `B`: `f` of (`a` times `b`) is equal to (`f` of `a`) times (`f` of `b`). This is a property of multiplicative homomorphisms.
More concisely: For any types `A`, `B` and equivalence relation on `A × A`, if `f` is a multiplicative homomorphism from the monoid of `A` under multiplication to the monoid of `B` under multiplication with respect to the relation, then `f` preserves multiplication, that is, `f(a × b) = f(a) × f(b)` for all `a, b` in `A`.
|
AddEquivClass.map_ne_zero_iff
theorem AddEquivClass.map_ne_zero_iff :
∀ {F : Type u_1} {M : Type u_12} {N : Type u_13} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : EquivLike F M N] [inst_3 : AddEquivClass F M N] (h : F) {x : M}, h x ≠ 0 ↔ x ≠ 0
This theorem, `AddEquivClass.map_ne_zero_iff`, states that for all types `F`, `M`, and `N`, given `M` and `N` are additive zero classes, `F` is an equivalence relation between `M` and `N`, and `F` is an additive equivalence class between `M` and `N`, for any instance `h` of `F` and any `x` in `M`, `h x` is not equal to zero if and only if `x` is not equal to zero. Essentially, it says that under these conditions, mapping `x` through the equivalence `h` preserves the property of not being zero.
More concisely: For all types `F`, `M`, and `N`, if `F` is an additive equivalence relation between additive zero classes `M` and `N`, then `x ∈ M` is not equal to zero if and only if `F x` is not equal to zero.
|
AddEquiv.ext
theorem AddEquiv.ext :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] {f g : M ≃+ N}, (∀ (x : M), f x = g x) → f = g := by
sorry
This theorem states that two additive isomorphisms, `f` and `g`, between two types `M` and `N` (with an additive structure), are equal if they yield the same result for every element `x` of type `M`. In other words, if for all `x` in `M`, `f(x)` equals `g(x)`, then `f` and `g` are the same additive isomorphism.
More concisely: If `f` and `g` are additive isomorphisms from type `M` to type `N` such that for all `x` in `M`, `f(x) = g(x)`, then `f = g`.
|
AddEquiv.symm_apply_apply
theorem AddEquiv.symm_apply_apply :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (x : M), e.symm (e x) = x
The theorem `AddEquiv.symm_apply_apply` states that for any two types `M` and `N` that have addition operations, and any isomorphism `e` between these types, applying `e` to an element of `M` and then applying the inverse of `e` (denoted as `AddEquiv.symm e`) results in the original element of `M`. In other words, the inverse of `e` is a left inverse of `e`, mathematically expressed as `e.symm (e y) = y` for any `y` in `M`.
More concisely: For any additive type isomorphism `e`: `e.symm (e x) = x` for all `x` in the domain of `e`.
|
MulEquiv.toMonoidHom_injective
theorem MulEquiv.toMonoidHom_injective :
∀ {M : Type u_6} {N : Type u_7} [inst : MulOneClass M] [inst_1 : MulOneClass N],
Function.Injective MulEquiv.toMonoidHom
The theorem `MulEquiv.toMonoidHom_injective` states that for any two types `M` and `N` that have the structures of multiplicative monoids (indicated by the typeclass `MulOneClass`), the function `MulEquiv.toMonoidHom` is injective. In other words, if two multiplicative equivalences between `M` and `N` are converted into multiplication-preserving functions (monoid homomorphisms) and these two resulting functions are found to be the same, then the original multiplicative equivalences must have been the same as well.
More concisely: If `f` and `g` are multiplicative equivalences between multiplicative monoids `M` and `N`, then `MulEquiv.toMonoidHom f` and `MulEquiv.toMonoidHom g` are equal if and only if `f` and `g` are equal.
|
MulEquiv.injective
theorem MulEquiv.injective :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Injective ⇑e
The theorem `MulEquiv.injective` states that for any two types `M` and `N` where `M` and `N` are equipped with a multiplication operation (i.e., they are instances of the `Mul` typeclass), any multiplicative equivalence `e` between `M` and `N` is an injective function. In other words, if `e` is such a multiplicative equivalence, then for any two elements `a₁` and `a₂` in `M`, if `e` of `a₁` equals `e` of `a₂`, it implies that `a₁` equals `a₂`. This theorem doesn't provide a proof, it's represented as `by sorry`.
More concisely: Given types `M` and `N` with multiplication operations, any multiplicative equivalence between `M` and `N` is a function with the property that if `e(a₁) = e(a₂)`, then `a₁ = a₂`.
|
AddEquivClass.map_eq_zero_iff
theorem AddEquivClass.map_eq_zero_iff :
∀ {F : Type u_1} {M : Type u_12} {N : Type u_13} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
[inst_2 : EquivLike F M N] [inst_3 : AddEquivClass F M N] (h : F) {x : M}, h x = 0 ↔ x = 0
The theorem `AddEquivClass.map_eq_zero_iff` states that for any types `F`, `M`, and `N`, where `M` and `N` are additive groups (i.e., they have a zero element and an addition operation), and `F` is a equivalence between `M` and `N` respecting the addition (i.e., it is an additive equivalence), then for any element `h` of type `F` and any element `x` of type `M`, `h x` equals zero if and only if `x` equals zero. In other words, additive equivalences preserve the zero element.
More concisely: For any additive groups M, N, and additive equivalence F between them, h ∈ F implies h(x) = 0 if and only if x = 0.
|
AddEquiv.apply_symm_apply
theorem AddEquiv.apply_symm_apply :
∀ {M : Type u_6} {N : Type u_7} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N) (y : N), e (e.symm y) = y
The theorem `AddEquiv.apply_symm_apply` states that for any isomorphism `e` from an additive group `M` to an additive group `N`, applying `e` to the result of applying the inverse of `e` (`e.symm`) to any element `y` of `N` returns `y` itself. In other words, the inverse of `e` (`e.symm`) is a right inverse of `e`, meaning that `e` followed by `e.symm` is the identity on `N`.
More concisely: For any additive group isomorphism `e` from `M` to `N`, `e (e.symm x) = x` for all `x` in `N`.
|
MulEquiv.map_inv
theorem MulEquiv.map_inv :
∀ {G : Type u_10} {H : Type u_11} [inst : Group G] [inst_1 : DivisionMonoid H] (h : G ≃* H) (x : G),
h x⁻¹ = (h x)⁻¹
This theorem states that a multiplicative equivalence between two groups, `G` and `H`, preserves the inversion operation. In other words, for any group element `x` in `G`, the inverse of `x` under the equivalence `h` is the same as the inverse of the image of `x` under `h` in `H`. This applies to any `G` and `H` where `G` is a group and `H` is a division monoid.
More concisely: If `h` is a multiplicative equivalence between groups `G` and `H`, then for all `x` in `G`, `h(x)^-1 = h(x^-1)` in `H`.
|
MulEquiv.map_mul
theorem MulEquiv.map_mul :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N) (x y : M), f (x * y) = f x * f y := by
sorry
This theorem states that a multiplicative isomorphism preserves the multiplication operation. Specifically, for any types `M` and `N` that have a multiplication operation (expressed by the `Mul` typeclass), if `f` is a multiplicative isomorphism from `M` to `N`, then the image of the product of any two elements `x` and `y` in `M` under `f` is the same as the product of the images of `x` and `y` under `f`. This is to say, applying the function `f` to the product `x * y` gives the same result as multiplying the results of applying `f` to `x` and `y` separately.
More concisely: Given multiplicative types M and N with multiplication operations, and a multiplicative isomorphism f : M → N, then for all x, y in M, f (x * y) = f x * f y.
|
MulEquiv.symm_symm
theorem MulEquiv.symm_symm :
∀ {M : Type u_6} {N : Type u_7} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), f.symm.symm = f
The theorem `MulEquiv.symm_symm` states that for any two types `M` and `N` which have a multiplication operation defined (denoted by `Mul M` and `Mul N` respectively), if there exists a multiplicative equivalence (isomorphism) `f` from type `M` to `N`, then the inverse of the inverse of this isomorphism `f` is equivalent to the original isomorphism `f`. In mathematical terms, this means if we have an isomorphism f : M -> N, then (f^{-1})^{-1} = f.
More concisely: If `f : M -> N` is a multiplicative equivalence between types `M` and `N`, then `f = (f^-\^{}-1)^-1`.
|