Documentation

Mathlib.Logic.Small.Group

Transfer group structures from α to Shrink α. #

instance instZeroShrink {α : Type u_1} [Zero α] [Small.{u_2, u_1} α] :
Equations
instance instOneShrink {α : Type u_1} [One α] [Small.{u_2, u_1} α] :
Equations
@[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} α] :
Equations
instance instMulShrink {α : Type u_1} [Mul α] [Small.{u_2, u_1} α] :
Equations
@[simp]
theorem equivShrink_symm_add {α : Type u_1} [Add α] [Small.{u_2, u_1} α] (x : Shrink.{u_2, u_1} α) (y : Shrink.{u_2, u_1} α) :
(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.{u_2, u_1} α) (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
instance instSubShrink {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] :
Equations
instance instDivShrink {α : Type u_1} [Div α] [Small.{u_2, u_1} α] :
Equations
@[simp]
theorem equivShrink_symm_sub {α : Type u_1} [Sub α] [Small.{u_2, u_1} α] (x : Shrink.{u_2, u_1} α) (y : Shrink.{u_2, u_1} α) :
(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.{u_2, u_1} α) (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
instance instNegShrink {α : Type u_1} [Neg α] [Small.{u_2, u_1} α] :
Equations
instance instInvShrink {α : Type u_1} [Inv α] [Small.{u_2, u_1} α] :
Equations
@[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_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.{u_2, u_1} α) :
(equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹
@[simp]
theorem equivShrink_inv {α : Type u_1} [Inv α] [Small.{u_2, u_1} α] (x : α) :
Equations
Equations
Equations
  • instSemigroupWithZeroShrink = (equivShrink α).symm.semigroupWithZero
Equations
  • instAddCommSemigroupShrink = (equivShrink α).symm.addCommSemigroup
Equations
  • instCommSemigroupShrink = (equivShrink α).symm.commSemigroup
Equations
Equations
Equations
Equations
  • instMulZeroOneClassShrink = (equivShrink α).symm.mulZeroOneClass
Equations
Equations
Equations
  • instAddCommMonoidShrink = (equivShrink α).symm.addCommMonoid
Equations
Equations
Equations
Equations
Equations