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 β)

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

A small module is linearly equivalent to its small model.

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

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

A small algebra is algebra equivalent to its small model.