Transfer group structures from α to Shrink α. #

instance instZeroShrink {α : Type u_1} [Zero α] [] :
Zero ()
Equations
• instZeroShrink = ().symm.zero
instance instOneShrink {α : Type u_1} [One α] [] :
One ()
Equations
• instOneShrink = ().symm.one
@[simp]
theorem equivShrink_symm_zero {α : Type u_1} [Zero α] [] :
().symm 0 = 0
@[simp]
theorem equivShrink_symm_one {α : Type u_1} [One α] [] :
().symm 1 = 1
Equations
instance instMulShrink {α : Type u_1} [Mul α] [] :
Mul ()
Equations
• instMulShrink = ().symm.mul
@[simp]
theorem equivShrink_symm_add {α : Type u_1} [Add α] [] (x : ) (y : ) :
().symm (x + y) = ().symm x + ().symm y
@[simp]
theorem equivShrink_add {α : Type u_1} [Add α] [] (x : α) (y : α) :
() (x + y) = () x + () y
@[simp]
theorem equivShrink_symm_mul {α : Type u_1} [Mul α] [] (x : ) (y : ) :
().symm (x * y) = ().symm x * ().symm y
@[simp]
theorem equivShrink_mul {α : Type u_1} [Mul α] [] (x : α) (y : α) :
() (x * y) = () x * () y
instance instSubShrink {α : Type u_1} [Sub α] [] :
Sub ()
Equations
• instSubShrink = ().symm.sub
instance instDivShrink {α : Type u_1} [Div α] [] :
Div ()
Equations
• instDivShrink = ().symm.div
@[simp]
theorem equivShrink_symm_sub {α : Type u_1} [Sub α] [] (x : ) (y : ) :
().symm (x - y) = ().symm x - ().symm y
@[simp]
theorem equivShrink_sub {α : Type u_1} [Sub α] [] (x : α) (y : α) :
() (x - y) = () x - () y
@[simp]
theorem equivShrink_symm_div {α : Type u_1} [Div α] [] (x : ) (y : ) :
().symm (x / y) = ().symm x / ().symm y
@[simp]
theorem equivShrink_div {α : Type u_1} [Div α] [] (x : α) (y : α) :
() (x / y) = () x / () y
instance instNegShrink {α : Type u_1} [Neg α] [] :
Neg ()
Equations
• instNegShrink = ().symm.Neg
instance instInvShrink {α : Type u_1} [Inv α] [] :
Inv ()
Equations
• instInvShrink = ().symm.Inv
@[simp]
theorem equivShrink_symm_neg {α : Type u_1} [Neg α] [] (x : ) :
().symm (-x) = -().symm x
@[simp]
theorem equivShrink_neg {α : Type u_1} [Neg α] [] (x : α) :
() (-x) = -() x
@[simp]
theorem equivShrink_symm_inv {α : Type u_1} [Inv α] [] (x : ) :
().symm x⁻¹ = (().symm x)⁻¹
@[simp]
theorem equivShrink_inv {α : Type u_1} [Inv α] [] (x : α) :
() x⁻¹ = (() x)⁻¹
instance instAddSemigroupShrink {α : Type u_1} [] [] :
Equations
instance instSemigroupShrink {α : Type u_1} [] [] :
Equations
• instSemigroupShrink = ().symm.semigroup
Equations
• instSemigroupWithZeroShrink = ().symm.semigroupWithZero
instance instAddCommSemigroupShrink {α : Type u_1} [] [] :
Equations
instance instCommSemigroupShrink {α : Type u_1} [] [] :
Equations
• instCommSemigroupShrink = ().symm.commSemigroup
instance instMulZeroClassShrink {α : Type u_1} [] [] :
Equations
• instMulZeroClassShrink = ().symm.mulZeroClass
instance instAddZeroClassShrink {α : Type u_1} [] [] :
Equations
instance instMulOneClassShrink {α : Type u_1} [] [] :
Equations
• instMulOneClassShrink = ().symm.mulOneClass
instance instMulZeroOneClassShrink {α : Type u_1} [] [] :
Equations
• instMulZeroOneClassShrink = ().symm.mulZeroOneClass
instance instAddMonoidShrink {α : Type u_1} [] [] :
Equations
instance instMonoidShrink {α : Type u_1} [] [] :
Equations
• instMonoidShrink = ().symm.monoid
instance instAddCommMonoidShrink {α : Type u_1} [] [] :
Equations
instance instCommMonoidShrink {α : Type u_1} [] [] :
Equations
• instCommMonoidShrink = ().symm.commMonoid
instance instAddGroupShrink {α : Type u_1} [] [] :
Equations