Transfer group structures from α to Shrink α.

instance instZeroShrink {α : Type u_1} [Zero α] [Small.{u_2, u_1} α] : Zero (Shrink α)

instance instOneShrink {α : Type u_1} [One α] [Small.{u_2, u_1} α] : One (Shrink α)

@[simp]

theorem equivShrink_symm_zero {α : Type u_1} [Zero α] [Small.{u_2, u_1} α] : ↑(equivShrink α).symm 0 = 0

@[simp]

theorem equivShrink_symm_one {α : Type u_1} [One α] [Small.{u_2, u_1} α] : ↑(equivShrink α).symm 1 = 1

instance instAddShrink {α : Type u_1} [Add α] [Small.{u_2, u_1} α] : Add (Shrink α)

instance instMulShrink {α : Type u_1} [Mul α] [Small.{u_2, u_1} α] : Mul (Shrink α)

@[simp]

theorem equivShrink_symm_add {α : Type u_1} [Add α] [Small.{u_2, u_1} α] (x : Shrink α) (y : Shrink α) : ↑(equivShrink α).symm (x + y) = ↑(equivShrink α).symm x + ↑(equivShrink α).symm y

@[simp]

theorem equivShrink_add {α : Type u_1} [Add α] [Small.{u_2, u_1} α] (x : α) (y : α) : ↑(equivShrink α) (x + y) = ↑(equivShrink α) x + ↑(equivShrink α) y

@[simp]

theorem equivShrink_symm_mul {α : Type u_1} [Mul α] [Small.{u_2, u_1} α] (x : Shrink α) (y : Shrink α) : ↑(equivShrink α).symm (x * y) = ↑(equivShrink α).symm x * ↑(equivShrink α).symm y

@[simp]

theorem equivShrink_mul {α : Type u_1} [Mul α] [Small.{u_2, u_1} α] (x : α) (y : α) : ↑(equivShrink α) (x * y) = ↑(equivShrink α) x * ↑(equivShrink α) y

instance instSubShrink {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] : Sub (Shrink α)

instance instDivShrink {α : Type u_1} [Div α] [Small.{u_2, u_1} α] : Div (Shrink α)

@[simp]

theorem equivShrink_symm_sub {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] (x : Shrink α) (y : Shrink α) : ↑(equivShrink α).symm (x - y) = ↑(equivShrink α).symm x - ↑(equivShrink α).symm y

@[simp]

theorem equivShrink_sub {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] (x : α) (y : α) : ↑(equivShrink α) (x - y) = ↑(equivShrink α) x - ↑(equivShrink α) y

@[simp]

theorem equivShrink_symm_div {α : Type u_1} [Div α] [Small.{u_2, u_1} α] (x : Shrink α) (y : Shrink α) : ↑(equivShrink α).symm (x / y) = ↑(equivShrink α).symm x / ↑(equivShrink α).symm y

@[simp]

theorem equivShrink_div {α : Type u_1} [Div α] [Small.{u_2, u_1} α] (x : α) (y : α) : ↑(equivShrink α) (x / y) = ↑(equivShrink α) x / ↑(equivShrink α) y

instance instNegShrink {α : Type u_1} [Neg α] [Small.{u_2, u_1} α] : Neg (Shrink α)

instance instInvShrink {α : Type u_1} [Inv α] [Small.{u_2, u_1} α] : Inv (Shrink α)

@[simp]

theorem equivShrink_symm_neg {α : Type u_1} [Neg α] [Small.{u_2, u_1} α] (x : Shrink α) : ↑(equivShrink α).symm (-x) = -↑(equivShrink α).symm x

@[simp]

theorem equivShrink_neg {α : Type u_1} [Neg α] [Small.{u_2, u_1} α] (x : α) : ↑(equivShrink α) (-x) = -↑(equivShrink α) x

@[simp]

theorem equivShrink_symm_inv {α : Type u_1} [Inv α] [Small.{u_2, u_1} α] (x : Shrink α) : ↑(equivShrink α).symm x⁻¹ = (↑(equivShrink α).symm x)⁻¹

@[simp]

theorem equivShrink_inv {α : Type u_1} [Inv α] [Small.{u_2, u_1} α] (x : α) : ↑(equivShrink α) x⁻¹ = (↑(equivShrink α) x)⁻¹

instance instAddSemigroupShrink {α : Type u_1} [AddSemigroup α] [Small.{u_2, u_1} α] : AddSemigroup (Shrink α)

instance instSemigroupShrink {α : Type u_1} [Semigroup α] [Small.{u_2, u_1} α] : Semigroup (Shrink α)

instance instSemigroupWithZeroShrink {α : Type u_1} [SemigroupWithZero α] [Small.{u_2, u_1} α] : SemigroupWithZero (Shrink α)

instance instAddCommSemigroupShrink {α : Type u_1} [AddCommSemigroup α] [Small.{u_2, u_1} α] : AddCommSemigroup (Shrink α)

instance instCommSemigroupShrink {α : Type u_1} [CommSemigroup α] [Small.{u_2, u_1} α] : CommSemigroup (Shrink α)

instance instMulZeroClassShrink {α : Type u_1} [MulZeroClass α] [Small.{u_2, u_1} α] : MulZeroClass (Shrink α)

instance instAddZeroClassShrink {α : Type u_1} [AddZeroClass α] [Small.{u_2, u_1} α] : AddZeroClass (Shrink α)

instance instMulOneClassShrink {α : Type u_1} [MulOneClass α] [Small.{u_2, u_1} α] : MulOneClass (Shrink α)

instance instMulZeroOneClassShrink {α : Type u_1} [MulZeroOneClass α] [Small.{u_2, u_1} α] : MulZeroOneClass (Shrink α)

instance instAddMonoidShrink {α : Type u_1} [AddMonoid α] [Small.{u_2, u_1} α] : AddMonoid (Shrink α)

instance instMonoidShrink {α : Type u_1} [Monoid α] [Small.{u_2, u_1} α] : Monoid (Shrink α)

instance instAddCommMonoidShrink {α : Type u_1} [AddCommMonoid α] [Small.{u_2, u_1} α] : AddCommMonoid (Shrink α)

instance instCommMonoidShrink {α : Type u_1} [CommMonoid α] [Small.{u_2, u_1} α] : CommMonoid (Shrink α)

instance instAddGroupShrink {α : Type u_1} [AddGroup α] [Small.{u_2, u_1} α] : AddGroup (Shrink α)

instance instGroupShrink {α : Type u_1} [Group α] [Small.{u_2, u_1} α] : Group (Shrink α)

instance instAddCommGroupShrink {α : Type u_1} [AddCommGroup α] [Small.{u_2, u_1} α] : AddCommGroup (Shrink α)

instance instCommGroupShrink {α : Type u_1} [CommGroup α] [Small.{u_2, u_1} α] : CommGroup (Shrink α)