Documentation

Mathlib.Logic.Small.Module

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

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

A small module is linearly equivalent to its small model.

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

    A small algebra is algebra equivalent to its small model.

    Equations
    Instances For