CompPoly

KO | EN

gitlite — search

#javascript #python #hacktoberfest #react #ai #typescript #llm #go #golang #android #machine-learning #rust #deep-learning #linux

(★ 10)

No description available.

CompPoly Latest Version Download

Download Latest Version (.zip)

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# CompPoly

A library for computational multivariate polynomial rings over a base commutative ring (or semiring), with variables indexed by natural numbers.

## Representation

A polynomial is represented by the type `CMvPolynomial (n : ℕ) (R : Type) [Zero R] : Type`, where `n` is the number of variables (indexed from 0) and `R` is the type of coefficients.

This polynomial representation is implemented internally as a map from monomials in `n` variables (`CMvMonomial (n : ℕ) : Type`) to coefficients, with the constraint that no monomial maps to the `0` coefficient.
This implementation is then shown to be equivalent with a Mathlib polynomial ring with `Fin n` variables. More specifically, we instantiate a `RingEquiv` structure (modulo some typeclass constraints) between our type and `MvPolynomial (Fin n) R` which is defined in `Mathlib.Algebra.MvPolynomial.Basic`.

## Importing the library

If your project is using a `lakefile.lean`, you can add
```
require CompPoly from git
  "https://github.com/NethermindEth/CompPoly"
```
or you can specify the exact commit, for example:
```
require CompPoly from git
  "https://github.com/NethermindEth/CompPoly"@"ede2290"
```
If your project is using a `lakefile.toml`, you can add
```
[[require]]
name = "CompPoly"
git = "https://github.com/NethermindEth/CompPoly"
```
or you can specify the exact commit, for example:
```
[[require]]
name = "CompPoly"
git = "https://github.com/NethermindEth/CompPoly"
rev = "ede2290"
```

Then you can import the desired modules, for example:
```lean
import CompPoly.CMvPolynomial
```
```lean
import CompPoly.MvPolyEquiv
```

## Current status and plans

So far we have defined counterparts for the following `MvPolynomial` definitions:
`C`, `coeff`, `commSemiring`, `decidableEqMvPolynomial`, `degreeOf`, `eval`, `eval₂`, `support` and `totalDegree`. Many have the same name and are located in the namespace `CPoly.CMvPolynomial`; some are defined on `Lawful`, which `CMvPolynomial` is an abbrev of.

For the future, we plan to add counterparts to `MonomialOrder.degree`, `MonomialOrder.leadingCoeff` and the following `MvPolynomial` definitions (but we're first assessing the implementation complexity for some of them): `X`, `aeval`, `algebra`, `bind₁`, `degrees`, `eval₂Hom`, `finSuccEquiv`, `instCommRingMvPolynomial`, `isEmptyAlgEquiv`, `module`, `monomial`, `optionEquivLeft`, `rename`, `renameEquiv`, `restrictDegree`, `smulZeroClass`, `sumToIter`, `vars`.

CompPoly

CompPoly Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

CompPoly

CompPoly Latest Version Download

Today's picks

Was this content helpful?

Recent Feedback

Download README