Degree.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The explicit polynomial has total degree five

The leading homogeneous part is -2 * Q^2 * (X 1 + X 3), of degree five. The remaining part has degree at most four. Nonvanishing is checked by ordinary evaluation, rather than assumed from a displayed expression.

theorem OAI.StableCoordinate.Q_isHomogeneous line 21
Source documentation
The quadratic form in the displayed formula is homogeneous of degree two.
```
theorem Q_isHomogeneous : Q.IsHomogeneous 2 := by
…
```
theorem OAI.StableCoordinate.Q_ne_zero line 28
Source documentation
Evaluate at (x₁,x₂,x₃,x₄)=(0,1,0,0).
```
theorem Q_ne_zero : Q ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.Q
theorem OAI.StableCoordinate.Q_totalDegree line 34
Source documentation
The source's quadratic auxiliary expression has exact degree two.
```
theorem Q_totalDegree : Q.totalDegree = 2 := Q_isHomogeneous.totalDegree Q_ne_zero
```
Mentions: OAI.StableCoordinate.Q_ne_zero
theorem OAI.StableCoordinate.x2_add_x4_ne_zero line 36
theorem OAI.StableCoordinate.f_totalDegree line 42
Source documentation
The exact degree-five property advertised by the principal target.
```
theorem f_totalDegree : f.totalDegree = 5 := by
…
```