OAI/Algebra/Finitistic/Localization/LocalizedEvaluationStructure.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.LittleFinitistic.QuadraticEncoding.boundedQ_triangulated line 12

   Source documentation

   The constructed quotient carries its canonical triangulated structure.

   theorem boundedQ_triangulated : IsTriangulated (BoundedQ P) := inferInstance
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.BoundedQ

2. instance OAI.LittleFinitistic.QuadraticEncoding.quotientEvaluationAdditive line 16
3. instance OAI.LittleFinitistic.QuadraticEncoding.quotientEvaluationLifting line 20
4. instance OAI.LittleFinitistic.QuadraticEncoding.quotientEvaluationShift line 25
5. instance OAI.LittleFinitistic.QuadraticEncoding.quotientEvaluationFactorsShift line 29
6. instance OAI.LittleFinitistic.QuadraticEncoding.quotientEvaluationTriangulated line 35