OAI/Algebra/Finitistic/Encoding/FiniteBasisIso.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.FiniteBasisIso.family line 11
2. def OAI.LittleFinitistic.FiniteBasisIso.iso line 14

   Source documentation

   An actual finite basis gives the scalar-column isomorphism, including the empty basis.

   def iso : (⨁ (family (k := k) : I → _)) ≅ ModuleCat.of k V :=
   …

   Mentions: OAI.LittleFinitistic.FiniteBasisIso.family

3. theorem OAI.LittleFinitistic.FiniteBasisIso.pi_hom_proj line 17
4. theorem OAI.LittleFinitistic.FiniteBasisIso.injection_apply line 23