Documentation

Mathlib.Algebra.Group.Shrink

Transfer group structures from α to Shrink α #

source
@[instance_reducible]
noncomputable instance Shrink.instOne {α : Type u_2} [Small.{v, u_2} α] [One α] :
One (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instZero {α : Type u_2} [Small.{v, u_2} α] [Zero α] :
Zero (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] :
Mul (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] :
Add (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instDiv {α : Type u_2} [Small.{v, u_2} α] [Div α] :
Div (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instSub {α : Type u_2} [Small.{v, u_2} α] [Sub α] :
Sub (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instInv {α : Type u_2} [Small.{v, u_2} α] [Inv α] :
Inv (Shrink.{v, u_2} α)
source
@[instance_reducible]
noncomputable instance Shrink.instNeg {α : Type u_2} [Small.{v, u_2} α] [Neg α] :
Neg (Shrink.{v, u_2} α)
source
@[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
source
@[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} α)
source
@[simp]
theorem equivShrink_symm_one {α : Type u_2} [Small.{v, u_2} α] [One α] :
(equivShrink α).symm 1 = 1
source
@[simp]
theorem equivShrink_symm_zero {α : Type u_2} [Small.{v, u_2} α] [Zero α] :
(equivShrink α).symm 0 = 0
source
@[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
source
@[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
source
@[simp]
theorem equivShrink_mul {α : Type u_2} [Small.{v, u_2} α] [Mul α] (x y : α) :
(equivShrink α) (x * y) = (equivShrink α) x * (equivShrink α) y
source
@[simp]
theorem equivShrink_add {α : Type u_2} [Small.{v, u_2} α] [Add α] (x y : α) :
(equivShrink α) (x + y) = (equivShrink α) x + (equivShrink α) y
source
@[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
source
@[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
source
@[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
source
@[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
source
@[simp]
theorem equivShrink_div {α : Type u_2} [Small.{v, u_2} α] [Div α] (x y : α) :
(equivShrink α) (x / y) = (equivShrink α) x / (equivShrink α) y
source
@[simp]
theorem equivShrink_sub {α : Type u_2} [Small.{v, u_2} α] [Sub α] (x y : α) :
(equivShrink α) (x - y) = (equivShrink α) x - (equivShrink α) y
source
@[simp]
theorem equivShrink_symm_inv {α : Type u_2} [Small.{v, u_2} α] [Inv α] (x : Shrink.{v, u_2} α) :
(equivShrink α).symm x⁻¹ = ((equivShrink α).symm x)⁻¹
source
@[simp]
theorem equivShrink_symm_neg {α : Type u_2} [Small.{v, u_2} α] [Neg α] (x : Shrink.{v, u_2} α) :
(equivShrink α).symm (-x) = -(equivShrink α).symm x
source
@[simp]
theorem equivShrink_inv {α : Type u_2} [Small.{v, u_2} α] [Inv α] (x : α) :
(equivShrink α) x⁻¹ = ((equivShrink α) x)⁻¹
source
@[simp]
theorem equivShrink_neg {α : Type u_2} [Small.{v, u_2} α] [Neg α] (x : α) :
(equivShrink α) (-x) = -(equivShrink α) x
source
noncomputable def Shrink.mulEquiv {α : Type u_2} [Small.{v, u_2} α] [Mul α] :
Shrink.{v, u_2} α ≃* α

Shrink α to a smaller universe preserves multiplication.

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

    Shrink α to a smaller universe preserves addition.

    Instances For
      source
      @[simp]
      theorem Shrink.addEquiv_apply {α : Type u_2} [Small.{v, u_2} α] [Add α] (a✝ : Shrink.{v, u_2} α) :
      addEquiv a✝ = (equivShrink α).symm a✝
      source
      @[simp]
      theorem Shrink.mulEquiv_symm_apply {α : Type u_2} [Small.{v, u_2} α] [Mul α] (a✝ : α) :
      mulEquiv.symm a✝ = (equivShrink α) a✝
      source
      @[simp]
      theorem Shrink.addEquiv_symm_apply {α : Type u_2} [Small.{v, u_2} α] [Add α] (a✝ : α) :
      addEquiv.symm a✝ = (equivShrink α) a✝
      source
      @[simp]
      theorem Shrink.mulEquiv_apply {α : Type u_2} [Small.{v, u_2} α] [Mul α] (a✝ : Shrink.{v, u_2} α) :
      mulEquiv a✝ = (equivShrink α).symm a✝
      source
      @[instance_reducible]
      noncomputable instance Shrink.instSemigroup {α : Type u_2} [Small.{v, u_2} α] [Semigroup α] :
      Semigroup (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddSemigroup {α : Type u_2} [Small.{v, u_2} α] [AddSemigroup α] :
      AddSemigroup (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instCommSemigroup {α : Type u_2} [Small.{v, u_2} α] [CommSemigroup α] :
      CommSemigroup (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddCommSemigroup {α : Type u_2} [Small.{v, u_2} α] [AddCommSemigroup α] :
      AddCommSemigroup (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsLeftCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsLeftCancelMul α] :
      IsLeftCancelMul (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsLeftCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsLeftCancelAdd α] :
      IsLeftCancelAdd (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsRightCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsRightCancelMul α] :
      IsRightCancelMul (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsRightCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsRightCancelAdd α] :
      IsRightCancelAdd (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsCancelMul {α : Type u_2} [Small.{v, u_2} α] [Mul α] [IsCancelMul α] :
      IsCancelMul (Shrink.{v, u_2} α)
      source
      instance Shrink.instIsCancelAdd {α : Type u_2} [Small.{v, u_2} α] [Add α] [IsCancelAdd α] :
      IsCancelAdd (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instMulOneClass {α : Type u_2} [Small.{v, u_2} α] [MulOneClass α] :
      MulOneClass (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddZeroClass {α : Type u_2} [Small.{v, u_2} α] [AddZeroClass α] :
      AddZeroClass (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instMonoid {α : Type u_2} [Small.{v, u_2} α] [Monoid α] :
      Monoid (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddMonoid {α : Type u_2} [Small.{v, u_2} α] [AddMonoid α] :
      AddMonoid (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instCommMonoid {α : Type u_2} [Small.{v, u_2} α] [CommMonoid α] :
      CommMonoid (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddCommMonoid {α : Type u_2} [Small.{v, u_2} α] [AddCommMonoid α] :
      AddCommMonoid (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instGroup {α : Type u_2} [Small.{v, u_2} α] [Group α] :
      Group (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddGroup {α : Type u_2} [Small.{v, u_2} α] [AddGroup α] :
      AddGroup (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instCommGroup {α : Type u_2} [Small.{v, u_2} α] [CommGroup α] :
      CommGroup (Shrink.{v, u_2} α)
      source
      @[instance_reducible]
      noncomputable instance Shrink.instAddCommGroup {α : Type u_2} [Small.{v, u_2} α] [AddCommGroup α] :
      AddCommGroup (Shrink.{v, u_2} α)
      source
      @[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} α)
      source
      @[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} α)