Least-Shifted-Degree Row Selection Helpers #
Correctness facts for the generic least-shifted-degree row scan in
PolynomialMatrix.Operations.
def
CompPoly.PolynomialMatrix.RowChoiceValid
{F : Type u_1}
[Field F]
[BEq F]
(M : PolynomialMatrix F)
(shift : Array ℕ)
(choice : RowChoice F)
:
Instances For
theorem
CompPoly.PolynomialMatrix.leastShiftedDegreeChoice?_some_valid
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{choice : RowChoice F}
(hchoice : M.leastShiftedDegreeChoice? shift = some choice)
:
M.RowChoiceValid shift choice
theorem
CompPoly.PolynomialMatrix.leastShiftedDegreeChoice?_degree_le
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{choice : RowChoice F}
{i d : ℕ}
(hchoice : M.leastShiftedDegreeChoice? shift = some choice)
(hi : i < Array.size M)
(hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some d)
:
theorem
CompPoly.PolynomialMatrix.leastShiftedDegreeChoice?_some_of_degree
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{i d : ℕ}
(hi : i < Array.size M)
(hdeg : rowShiftedDegree? (Array.getD M i #[]) shift = some d)
:
theorem
CompPoly.PolynomialMatrix.leastShiftedDegreeRow?_some_valid
{F : Type u_1}
[Field F]
[BEq F]
{M : PolynomialMatrix F}
{shift : Array ℕ}
{row : PolynomialRow F}
(hrow : M.leastShiftedDegreeRow? shift = some row)
:
∃ (choice : RowChoice F),
M.leastShiftedDegreeChoice? shift = some choice ∧ M.RowChoiceValid shift choice ∧ choice.row = row