Documentation

Mathlib.Logic.Small.Module

Transfer module and algebra structures from α to Shrink α. #

instance instModuleShrink {α : Type u_1} {β : Type u_2} [Semiring α] [AddCommMonoid β] [Module α β] [Small.{u_3, u_2} β] :
Equations
def linearEquivShrink (α : Type u_3) (β : Type u_4) [Semiring α] [AddCommMonoid β] [Module α β] [Small.{u_5, u_4} β] :

A small module is linearly equivalent to its small model.

Equations
Instances For
    instance instAlgebraShrink {α : Type u_1} {β : Type u_2} [CommSemiring α] [Semiring β] [Algebra α β] [Small.{u_3, u_2} β] :
    Equations
    def algEquivShrink (α : Type u_3) (β : Type u_4) [CommSemiring α] [Semiring β] [Algebra α β] [Small.{u_5, u_4} β] :

    A small algebra is algebra equivalent to its small model.

    Equations
    Instances For