Transfer module and algebra structures from α to Shrink α

instance Shrink.instModule {R : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] : Module R (Shrink.{v, u_2} α)

Equations

• Shrink.instModule = Equiv.module R (equivShrink α).symm

def Shrink.linearEquiv (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] : Shrink.{v, u_2} α ≃ₗ[R] α

Shrinking α to a smaller universe preserves module structure.

Equations

• Shrink.linearEquiv R α = Equiv.linearEquiv R (equivShrink α).symm

@[simp]

theorem Shrink.linearEquiv_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : Shrink.{v, u_2} α) : (linearEquiv R α) a✝ = (equivShrink α).symm a✝

@[simp]

theorem Shrink.linearEquiv_symm_apply (R : Type u_1) (α : Type u_2) [Small.{v, u_2} α] [Semiring R] [AddCommMonoid α] [Module R α] (a✝ : α) : (linearEquiv R α).symm a✝ = (equivShrink α) a✝