OAI/Algebra/FinitisticAsymmetry/Triangular/InjectiveCorners.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.CummingsConstruction.cval line 16
  2. def OAI.LittleFinitistic.CummingsConstruction.ehead line 17
  3. def OAI.LittleFinitistic.CummingsConstruction.etail line 18
  4. def OAI.LittleFinitistic.CummingsConstruction.oval line 19
  5. lemma OAI.LittleFinitistic.CummingsConstruction.cval_mul line 21
  6. lemma OAI.LittleFinitistic.CummingsConstruction.ehead_mul line 24
  7. lemma OAI.LittleFinitistic.CummingsConstruction.etail_mul line 25
  8. lemma OAI.LittleFinitistic.CummingsConstruction.oval_mul line 30
  9. def OAI.LittleFinitistic.CummingsConstruction.NewInjective line 32
  10. def OAI.LittleFinitistic.CummingsConstruction.NewInjective.value line 35
  11. lemma OAI.LittleFinitistic.CummingsConstruction.NewInjective.ext line 37
  12. instance OAI.LittleFinitistic.CummingsConstruction.NewInjective.(instance at line 42) line 42
  13. def OAI.LittleFinitistic.CummingsConstruction.NewInjective.act line 44
  14. instance OAI.LittleFinitistic.CummingsConstruction.NewInjective.(instance at line 49) line 49
  15. instance OAI.LittleFinitistic.CummingsConstruction.NewInjective.(instance at line 51) line 51
  16. def OAI.LittleFinitistic.CummingsConstruction.newIdem line 100
  17. lemma OAI.LittleFinitistic.CummingsConstruction.newIdem_mul line 102
  18. lemma OAI.LittleFinitistic.CummingsConstruction.field_module_injective line 134
  19. abbrev OAI.LittleFinitistic.CummingsConstruction.coindField line 143
  20. instance OAI.LittleFinitistic.CummingsConstruction.coindField_injective line 145
  21. lemma OAI.LittleFinitistic.CummingsConstruction.coindField_smul_eval line 150
  22. lemma OAI.LittleFinitistic.CummingsConstruction.coindField_add_eval line 161
  23. def OAI.LittleFinitistic.CummingsConstruction.newInjectiveRetraction line 166
  24. def OAI.LittleFinitistic.CummingsConstruction.lastCoordinate line 191
  25. def OAI.LittleFinitistic.CummingsConstruction.newInjectiveInclusion line 204
  26. lemma OAI.LittleFinitistic.CummingsConstruction.newInjectiveInclusion_apply line 208
  27. lemma OAI.LittleFinitistic.CummingsConstruction.newInjectiveInclusion_retraction line 216
  28. lemma OAI.LittleFinitistic.CummingsConstruction.newInjective_injective line 239