OAI/Algebra/Finitistic/Encoding/RelationPathCoordinates.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.LittleFinitistic.RelationPathCoordinates.coordinates line 11
2. theorem OAI.LittleFinitistic.RelationPathCoordinates.relation_coordinate line 15

   Source documentation

   The coefficient matrix of an actual relation, grouped by its first traversed arrow.

   theorem relation_coordinate (r : relationSpace P) (a : Fin (d+1)) :
       coordinates (r : Paths k d) a = ∑ b, coefficient P r a b • basis b := by
   …

   Mentions: OAI.LittleFinitistic.RelationPathCoordinates.coordinates

3. theorem OAI.LittleFinitistic.RelationPathCoordinates.basis_coordinate line 22

   Source documentation

   The actual independent relation basis has precisely the manuscript's q coefficients.

   theorem basis_coordinate (r : RelationIndex P) (a : Fin (d+1)) :
       coordinates ((RelationSequence.relationBasis P r : relationSpace P) : Paths k d) a =
         ∑ b, basisCoefficient P r a b • basis b :=
   …

   Mentions: OAI.LittleFinitistic.RelationPathCoordinates.coordinates, OAI.LittleFinitistic.RelationSequence.relationBasis