mathlib3 documentation

algebra.category.Group.equivalence_Group_AddGroup

Equivalence between Group and AddGroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains two equivalences:

The functor GroupAddGroup by sending X ↦ additive X and f ↦ f.

Equations

The functor CommGroupAddCommGroup by sending X ↦ additive X and f ↦ f.

Equations

The functor AddGroupGroup by sending X ↦ multiplicative Y and f ↦ f.

Equations

The functor AddCommGroupCommGroup by sending X ↦ multiplicative Y and f ↦ f.

Equations
@[simp]
theorem Group_AddGroup_equivalence_inverse_obj_str_zpow (X : AddGroup) (ᾰ : ) (ᾰ_1 : multiplicative X) :
group.zpow ᾰ_1 = ᾰ_1 ^
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_add (X : Group) (ᾰ ᾰ_1 : additive X) :
+ ᾰ_1 = sub_neg_monoid.add ᾰ_1
@[simp]
@[simp]
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_zsmul (X : Group) (ᾰ : ) (ᾰ_1 : additive X) :
add_group.zsmul ᾰ_1 = ᾰ_1
@[simp]
theorem Group_AddGroup_equivalence_functor_obj_str_sub (X : Group) (ᾰ ᾰ_1 : additive X) :
- ᾰ_1 = sub_neg_monoid.sub ᾰ_1
@[simp]
@[simp]
@[simp]
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_add (X : CommGroup) (ᾰ ᾰ_1 : additive X) :
+ ᾰ_1 = add_group.add ᾰ_1
@[simp]
theorem CommGroup_AddCommGroup_equivalence_functor_obj_str_sub (X : CommGroup) (ᾰ ᾰ_1 : additive X) :
- ᾰ_1 = add_group.sub ᾰ_1
@[simp]