Transfer module and algebra structures from α to Shrink α.

instance instModuleShrinkInstAddCommMonoidShrink {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] [Small.{u_3, u_2} β] : Module α (Shrink.{u_3, u_2} β)

Equations

• instModuleShrinkInstAddCommMonoidShrink = Equiv.module α (equivShrink β).symm

def linearEquivShrink (α : Type u_1) (β : Type u_2) [Semiring α] [AddCommMonoid β] [Module α β] [Small.{u_3, u_2} β] : β ≃ₗ[α] Shrink.{u_3, u_2} β

A small module is linearly equivalent to its small model.

Equations

• linearEquivShrink α β = LinearEquiv.symm (Equiv.linearEquiv α (equivShrink β).symm)

instance instAlgebraShrinkInstSemiringShrink {α : Type u_1} {β : Type u_2} [CommSemiring α] [Semiring β] [Algebra α β] [Small.{u_3, u_2} β] : Algebra α (Shrink.{u_3, u_2} β)

Equations

• instAlgebraShrinkInstSemiringShrink = Equiv.algebra α (equivShrink β).symm

def algEquivShrink (α : Type u_1) (β : Type u_2) [CommSemiring α] [Semiring β] [Algebra α β] [Small.{u_3, u_2} β] : β ≃ₐ[α] Shrink.{u_3, u_2} β

A small algebra is algebra equivalent to its small model.

Equations

• algEquivShrink α β = AlgEquiv.symm (Equiv.algEquiv α (equivShrink β).symm)