`OAI/Algebra/Finitistic/Ordinary/OrdinaryFinitePiSupport.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.FinitePiSupport.equivalence line 12
Source documentation
A product with all but one coordinate zero is exactly its remaining coordinate.
```
def equivalence : (∀ i, V i) ≃ₗ[R] V i₀ :=
…
```
theorem OAI.LittleFinitistic.FinitePiSupport.equivalence_apply line 24