RelationBasisCoefficients.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.RelationBasisCoefficients.pathBasis line 12
Source documentation
The actual ordered length-two path basis, with the later arrow first.
```
def pathBasis : Module.Basis (Fin (d+1) × Fin (d+1)) k (Paths k d) :=
…
```
def OAI.LittleFinitistic.RelationBasisCoefficients.coefficient line 16
Source documentation
Coefficient of the path b a in a vector of the actual relation subspace.
```
def coefficient (r : relationSpace P) (a b : Fin (d+1)) : k :=
…
```
theorem OAI.LittleFinitistic.RelationBasisCoefficients.expansion line 19
theorem OAI.LittleFinitistic.RelationBasisCoefficients.algebra_relation line 27
Source documentation
Every vector in the chosen relation basis gives the genuine algebra equation.
```
theorem algebra_relation (r : relationSpace P) :
    (∑ a, ∑ b, coefficient P r a b • (arrow12 P b * arrow01 P a)) = 0 := by
…
```
Mentions: OAI.LittleFinitistic.RelationBasisCoefficients.coefficient
abbrev OAI.LittleFinitistic.RelationBasisCoefficients.RelationIndex line 33
def OAI.LittleFinitistic.RelationBasisCoefficients.basisCoefficient line 35
theorem OAI.LittleFinitistic.RelationBasisCoefficients.basis_relation line 38