Transfer group structures from α to Shrink α.

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

Equations

• instOneShrink = (equivShrink α).symm.one

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

Equations

• instZeroShrink = (equivShrink α).symm.zero

@[simp]

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

@[simp]

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

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

Equations

• instMulShrink = (equivShrink α).symm.mul

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

Equations

• instAddShrink = (equivShrink α).symm.add

@[simp]

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

@[simp]

theorem equivShrink_symm_add {α : Type u_1} [Add α] [Small.{u_2, u_1} α] (x y : Shrink.{u_2, u_1} α) : (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

@[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_smul {α : Type u_1} {R : Type u_2} [SMul R α] [Small.{u_3, u_1} α] (r : R) (x : Shrink.{u_3, u_1} α) : (equivShrink α).symm (r • x) = r • (equivShrink α).symm x

@[simp]

theorem equivShrink_smul {α : Type u_1} {R : Type u_2} [SMul R α] [Small.{u_3, u_1} α] (r : R) (x : α) : (equivShrink α) (r • x) = r • (equivShrink α) x

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

Equations

• instDivShrink = (equivShrink α).symm.div

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

Equations

• instSubShrink = (equivShrink α).symm.sub

@[simp]

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

@[simp]

theorem equivShrink_symm_sub {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] (x y : Shrink.{u_2, u_1} α) : (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

@[simp]

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

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

Equations

• instInvShrink = (equivShrink α).symm.Inv

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

Equations

• instNegShrink = (equivShrink α).symm.Neg

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• instSemigroupShrink = (equivShrink α).symm.semigroup

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

Equations

• instAddSemigroupShrink = (equivShrink α).symm.addSemigroup

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

Equations

• instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero

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

Equations

• instCommSemigroupShrink = (equivShrink α).symm.commSemigroup

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

Equations

• instAddCommSemigroupShrink = (equivShrink α).symm.addCommSemigroup

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

Equations

• instMulZeroClassShrink = (equivShrink α).symm.mulZeroClass

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

Equations

• instMulOneClassShrink = (equivShrink α).symm.mulOneClass

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

Equations

• instAddZeroClassShrink = (equivShrink α).symm.addZeroClass

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

Equations

• instMulZeroOneClassShrink = (equivShrink α).symm.mulZeroOneClass

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

Equations

• instMonoidShrink = (equivShrink α).symm.monoid

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

Equations

• instAddMonoidShrink = (equivShrink α).symm.addMonoid

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

Equations

• instCommMonoidShrink = (equivShrink α).symm.commMonoid

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

Equations

• instAddCommMonoidShrink = (equivShrink α).symm.addCommMonoid

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

Equations

• instGroupShrink = (equivShrink α).symm.group

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

Equations

• instAddGroupShrink = (equivShrink α).symm.addGroup

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

Equations

• instCommGroupShrink = (equivShrink α).symm.commGroup

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

Equations

• instAddCommGroupShrink = (equivShrink α).symm.addCommGroup