QuadraticCoefficients.lean`

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.LittleFinitistic.QuadraticPresentation.Term line 10
def OAI.LittleFinitistic.QuadraticPresentation.term line 12
theorem OAI.LittleFinitistic.QuadraticPresentation.degreeLE_two_eq_span line 19
Source documentation
The degree bound is exactly the span of constants, generators, and ordered products of two generators. The two factors are never commuted.
```
theorem degreeLE_two_eq_span :
    degreeLE R α 2 = Submodule.span R (Set.range (term R α)) := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticPresentation.degreeLE, OAI.LittleFinitistic.QuadraticPresentation.term
def OAI.LittleFinitistic.QuadraticPresentation.coefficientPolynomial line 42
Source documentation
Finite coefficient form, suitable for the source's homogenization rule.
```
def coefficientPolynomial [Fintype α] (c : R) (l : α → R) (q : α → α → R) :
    FreeAlgebra R α :=
…
```
theorem OAI.LittleFinitistic.QuadraticPresentation.exists_coefficients line 48
theorem OAI.LittleFinitistic.QuadraticPresentation.coefficientPolynomial_degree line 58
theorem OAI.LittleFinitistic.QuadraticPresentation.degreeLE_two_iff_coefficients line 71
Source documentation
An exact characterization; the degree predicate hides no higher terms.
```
theorem degreeLE_two_iff_coefficients [Fintype α] (p : FreeAlgebra R α) :
    p ∈ degreeLE R α 2 ↔
      ∃ (c : R) (l : α → R) (q : α → α → R), coefficientPolynomial R α c l q = p := by
…
```
Mentions: OAI.LittleFinitistic.QuadraticPresentation.degreeLE, OAI.LittleFinitistic.QuadraticPresentation.coefficientPolynomial
theorem OAI.LittleFinitistic.QuadraticPresentation.relation_coefficients line 80
Source documentation
Every new quadratic relation has explicit constant, linear, and ordered quadratic coefficients, with a simultaneous choice for the whole finite family.
```
theorem relation_coefficients [Finite α] {κ : Type*} (p : κ → FreeAlgebra R α) (N : ℕ) :
    letI := Fintype.ofFinite (Letter α N)
…
```
Mentions: OAI.LittleFinitistic.QuadraticPresentation.Letter