Documentation

Mathlib.Algebra.Algebra.Shrink

Transfer module and algebra structures from α to Shrink α #

source
🔸 coverage
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} α)
Equations
    source
    🔸 coverage
    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.

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