EvaluationFromAlgebra.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.LittleFinitistic.QuadraticEncoding.Relations.Satisfies line 12
Source documentation
The displayed finite list of quadratic equations, in an arbitrary k-algebra.
```
def Relations.Satisfies (x : Fin d → R) : Prop := ∀ j,
…
```
def OAI.LittleFinitistic.QuadraticEncoding.Representation.ofAction line 20
Source documentation
Evaluate the quadratic presentation in any actual algebra action.
```
def ofAction (x : Fin d → R) (hx : P.Satisfies x) (ρ : R →ₐ[k] Module.End k Y) :
    Representation P Y where
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Representation
def OAI.LittleFinitistic.QuadraticEncoding.Representation.ofModule line 28
Source documentation
In particular, every R-module supplies the required representation.
```
def ofModule (x : Fin d → R) (hx : P.Satisfies x)
    [Module R Y] [IsScalarTower k R Y] : Representation P Y :=
…
```
Mentions: OAI.LittleFinitistic.QuadraticEncoding.Representation
theorem OAI.LittleFinitistic.QuadraticEncoding.Representation.ofModule_generator line 32