Documentation

Mathlib.Algebra.Module.Shrink

Transfer module and algebra structures from α to Shrink α #

source
🔸 coverage
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
    source
    🔸 coverage
    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
      Instances For
        source
        📐 coverage
        @[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✝
        source
        📐 coverage
        @[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✝