Transfer module and algebra structures from α to Shrink α

@[instance_reducible]

noncomputable 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 = { toMulAction := Shrink.instMulAction, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable 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 α = AddEquiv.linearEquiv R Shrink.addEquiv

@[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✝

@[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✝