OrdinaryTensorRightRestriction.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.TwoSidedTensor.rightRestriction line 21
Source documentation
The actual outside right action obtained by restricting the enveloping action.
```
abbrev rightRestriction : ModuleCat.{u} Bᵐᵒᵖ :=
…
```
def OAI.LittleFinitistic.TwoSidedTensor.rightActionEquiv line 26
Source documentation
The one-sided right tensor action equals the restriction of the genuine two-sided action.
```
def rightActionEquiv : RightTensor k A B M N ≃ₗ[Bᵐᵒᵖ] rightRestriction k A B S M N where
…
```
Mentions: OAI.LittleFinitistic.RightTensor, OAI.LittleFinitistic.TwoSidedTensor.rightRestriction