OAI/Algebra/Finitistic/Ordinary/OrdinaryPairComplex.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LittleFinitistic.PairComplex.complex line 14
2. theorem OAI.LittleFinitistic.PairComplex.complex_d line 24
3. def OAI.LittleFinitistic.PairComplex.fst line 29
4. def OAI.LittleFinitistic.PairComplex.snd line 37
5. def OAI.LittleFinitistic.PairComplex.inl line 45
6. def OAI.LittleFinitistic.PairComplex.inr line 56
7. theorem OAI.LittleFinitistic.PairComplex.inl_fst line 67
8. theorem OAI.LittleFinitistic.PairComplex.inl_snd line 68
9. theorem OAI.LittleFinitistic.PairComplex.inr_fst line 69
10. theorem OAI.LittleFinitistic.PairComplex.inr_snd line 70
11. def OAI.LittleFinitistic.PairComplex.biprodIso line 73

    Source documentation

    The actual coordinate complex is the native binary biproduct.

    def biprodIso : complex O T ≅ O ⊞ T where
    …

    Mentions: OAI.LittleFinitistic.PairComplex.complex