Transfer group structures from α to Shrink α

@[instance_reducible]

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

Equations

• Shrink.instOne = (equivShrink α).symm.one

@[instance_reducible]

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

Equations

• Shrink.instZero = (equivShrink α).symm.zero

@[instance_reducible]

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

Equations

• Shrink.instMul = (equivShrink α).symm.mul

@[instance_reducible]

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

Equations

• Shrink.instAdd = (equivShrink α).symm.add

@[instance_reducible]

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

Equations

• Shrink.instDiv = (equivShrink α).symm.div

@[instance_reducible]

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

Equations

• Shrink.instSub = (equivShrink α).symm.sub

@[instance_reducible]

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

Equations

• Shrink.instInv = (equivShrink α).symm.Inv

@[instance_reducible]

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

Equations

• Shrink.instNeg = (equivShrink α).symm.Neg

@[instance_reducible]

noncomputable instance Shrink.instPow {M : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [Pow α M] : Pow (Shrink.{v, u_2} α) M

Equations

• Shrink.instPow = Equiv.pow M (equivShrink α).symm

@[instance_reducible]

noncomputable instance Shrink.instNSMul {M : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [SMul M α] : SMul M (Shrink.{v, u_2} α)

Equations

• Shrink.instNSMul = Equiv.smul M (equivShrink α).symm

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem equivShrink_symm_smul {α : Type u_2} [Small.{v, u_2} α] {M : Type u_3} [SMul M α] (m : M) (x : Shrink.{v, u_2} α) : (equivShrink α).symm (m • x) = m • (equivShrink α).symm x

@[simp]

theorem equivShrink_smul {α : Type u_2} [Small.{v, u_2} α] {M : Type u_3} [SMul M α] (m : M) (x : α) : (equivShrink α) (m • x) = m • (equivShrink α) x

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def Shrink.mulEquiv {α : Type u_2} [Small.{v, u_2} α] [Mul α] : Shrink.{v, u_2} α ≃* α

Shrink α to a smaller universe preserves multiplication.

Equations

• Shrink.mulEquiv = (equivShrink α).symm.mulEquiv

noncomputable def Shrink.addEquiv {α : Type u_2} [Small.{v, u_2} α] [Add α] : Shrink.{v, u_2} α ≃+ α

Shrink α to a smaller universe preserves addition.

Equations

• Shrink.addEquiv = (equivShrink α).symm.addEquiv

@[simp]

theorem Shrink.addEquiv_apply {α : Type u_2} [Small.{v, u_2} α] [Add α] (a✝ : Shrink.{v, u_2} α) : addEquiv a✝ = (equivShrink α).symm a✝

@[simp]

theorem Shrink.mulEquiv_symm_apply {α : Type u_2} [Small.{v, u_2} α] [Mul α] (a✝ : α) : mulEquiv.symm a✝ = (equivShrink α) a✝

@[simp]

theorem Shrink.addEquiv_symm_apply {α : Type u_2} [Small.{v, u_2} α] [Add α] (a✝ : α) : addEquiv.symm a✝ = (equivShrink α) a✝

@[simp]

theorem Shrink.mulEquiv_apply {α : Type u_2} [Small.{v, u_2} α] [Mul α] (a✝ : Shrink.{v, u_2} α) : mulEquiv a✝ = (equivShrink α).symm a✝

@[instance_reducible]

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

Equations

• Shrink.instSemigroup = { toMul := Shrink.instMul, mul_assoc := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddSemigroup = { toAdd := Shrink.instAdd, add_assoc := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instCommSemigroup = { toSemigroup := Shrink.instSemigroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddCommSemigroup = { toAddSemigroup := Shrink.instAddSemigroup, add_comm := ⋯ }

instance Shrink.instIsLeftCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsLeftCancelMul α] : IsLeftCancelMul (Shrink.{v, u_2} α)

instance Shrink.instIsLeftCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsLeftCancelAdd α] : IsLeftCancelAdd (Shrink.{v, u_2} α)

instance Shrink.instIsRightCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsRightCancelMul α] : IsRightCancelMul (Shrink.{v, u_2} α)

instance Shrink.instIsRightCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsRightCancelAdd α] : IsRightCancelAdd (Shrink.{v, u_2} α)

instance Shrink.instIsCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsCancelMul α] : IsCancelMul (Shrink.{v, u_2} α)

instance Shrink.instIsCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsCancelAdd α] : IsCancelAdd (Shrink.{v, u_2} α)

@[instance_reducible]

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

Equations

• Shrink.instMulOneClass = { toOne := Shrink.instOne, toMul := Shrink.instMul, one_mul := ⋯, mul_one := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddZeroClass = { toZero := Shrink.instZero, toAdd := Shrink.instAdd, zero_add := ⋯, add_zero := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instMonoid = { toOne := Shrink.instOne, toMul := Shrink.instMul, mul_assoc := ⋯, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddMonoid = { toZero := Shrink.instZero, toAdd := Shrink.instAdd, add_assoc := ⋯, zero_add := ⋯, add_zero := ⋯, toNSMul := NSMul.ofSMul, nsmul_zero := ⋯, nsmul_succ := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instCommMonoid = { toMonoid := Shrink.instMonoid, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddCommMonoid = { toAddMonoid := Shrink.instAddMonoid, add_comm := ⋯ }

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

Equations

• Shrink.instCommGroup = { toGroup := Shrink.instGroup, mul_comm := ⋯ }

@[instance_reducible]

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

Equations

• Shrink.instAddCommGroup = { toAddGroup := Shrink.instAddGroup, add_comm := ⋯ }

@[instance_reducible]

noncomputable instance Shrink.instMulAction {M : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [Monoid M] [MulAction M α] : MulAction M (Shrink.{v, u_2} α)

Equations

• Shrink.instMulAction = Equiv.mulAction M (equivShrink α).symm

@[instance_reducible]

noncomputable instance Shrink.instAddAction {M : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [AddMonoid M] [AddAction M α] : AddAction M (Shrink.{v, u_2} α)

Equations

• Shrink.instAddAction = Equiv.addAction M (equivShrink α).symm