# Documentation

Mathlib.Logic.Small.Group

# Transfer group structures from α to Shrink α. #

instance instZeroShrink {α : Type u_1} [Zero α] [] :
Zero ()
instance instOneShrink {α : Type u_1} [One α] [] :
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
instance instMulShrink {α : Type u_1} [Mul α] [] :
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 ()
instance instDivShrink {α : Type u_1} [Div α] [] :
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 ()
instance instInvShrink {α : Type u_1} [Inv α] [] :
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} [] [] :
instance instSemigroupShrink {α : Type u_1} [] [] :
instance instSemigroupWithZeroShrink {α : Type u_1} [] :
instance instAddCommSemigroupShrink {α : Type u_1} [] [] :
instance instCommSemigroupShrink {α : Type u_1} [] [] :
instance instMulZeroClassShrink {α : Type u_1} [] [] :
instance instAddZeroClassShrink {α : Type u_1} [] [] :
instance instMulOneClassShrink {α : Type u_1} [] [] :
instance instMulZeroOneClassShrink {α : Type u_1} [] [] :
instance instAddMonoidShrink {α : Type u_1} [] [] :
instance instMonoidShrink {α : Type u_1} [] [] :
instance instAddCommMonoidShrink {α : Type u_1} [] [] :
instance instCommMonoidShrink {α : Type u_1} [] [] :
instance instAddGroupShrink {α : Type u_1} [] [] :
instance instGroupShrink {α : Type u_1} [] [] :
instance instAddCommGroupShrink {α : Type u_1} [] [] :
instance instCommGroupShrink {α : Type u_1} [] [] :