Transfer module and algebra structures from α to Shrink α

@[implicit_reducible]

noncomputable instance Shrink.instAlgebra {R : Type u_1} {α : Type u_2} [Small.{v, u_2} α] [CommSemiring R] [Semiring α] [Algebra R α] : Algebra R (Shrink.{v, u_2} α)

noncomputable def Shrink.algEquiv (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] : Shrink.{v, u_2} α ≃ₐ[R] α

Shrinking α to a smaller universe preserves algebra structure.

@[simp]

theorem Shrink.algEquiv_apply (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] (a✝ : Shrink.{v, u_2} α) : (algEquiv R α) a✝ = (equivShrink α).symm a✝

@[simp]

theorem Shrink.algEquiv_symm_apply (R : Type u_1) (α : Type u_2) [CommSemiring R] [Small.{v, u_2} α] [Semiring α] [Algebra R α] (a✝ : α) : (algEquiv R α).symm a✝ = (equivShrink α) a✝