PolynomialShift.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem346.PolynomialShift.derivation line 18
Source documentation
Transfer one unit of polynomial degree from src to dst. Other blocks are spectator variables.
```
def derivation (src dst : B) :
    Derivation K (MvPolynomial (B × I) K) (MvPolynomial (B × I) K) := by
…
```
theorem OAI.Problem346.PolynomialShift.derivation_X line 25
def OAI.Problem346.PolynomialShift.shift line 32
Source documentation
The directional shift as a linear endomorphism.
```
def shift (src dst : B) : Module.End K (MvPolynomial (B × I) K) :=
…
```
theorem OAI.Problem346.PolynomialShift.shift_apply line 36
def OAI.Problem346.PolynomialShift.euler line 40
Source documentation
Euler's operator for one block.
```
def euler (block : B) : Module.End K (MvPolynomial (B × I) K) :=
…
```
theorem OAI.Problem346.PolynomialShift.commutator line 43
theorem OAI.Problem346.PolynomialShift.commutator_apply line 52
theorem OAI.Problem346.PolynomialShift.weight_commutator line 60