OAI/Algebra/Finitistic/Localization/NormalizedQuotientAction.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.QuadraticEncoding.quotient_arrow12 line 10
2. def OAI.LittleFinitistic.QuadraticEncoding.normalizePath line 16

   Source documentation

   Divide each homogenized path by s's on the target side.

   def normalizePath : (vertexQ P 0 ⟶ vertexQ P 2) →ₗ[k] End (vertexQ P 0) where
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.vertexQ

3. lemma OAI.LittleFinitistic.QuadraticEncoding.normalizePath_quadratic line 21
4. lemma OAI.LittleFinitistic.QuadraticEncoding.normalizePath_linear line 29
5. lemma OAI.LittleFinitistic.QuadraticEncoding.normalizePath_constant line 34
6. theorem OAI.LittleFinitistic.QuadraticEncoding.normalizedGenerator_satisfies line 40

   Source documentation

   The original, inhomogeneous relations hold on L in the actual quotient.

   theorem normalizedGenerator_satisfies : P.Satisfies (normalizedGenerator P) := by
   …

   Mentions: OAI.LittleFinitistic.QuadraticEncoding.normalizedGenerator