Canonical representatives for the quotient F_p[X] / (g), reduced modulo
a monic positive-degree modulus.
- val : FpPoly p
The chosen representative polynomial, of degree below
g. The representative's degree is strictly below that of the modulus
g.
Instances For
Two quotient elements are equal when their underlying representatives
agree; the extensionality principle for Quotient g.
Reduce a polynomial to its canonical quotient representative.
Equations
- Hex.FpPoly.Quotient.reduce f = { val := g.modByMonic f hmonic, reduced := ⋯ }
Instances For
The stored representative of reduce f is the monic remainder computed by
the executable reduction path.
The stored representative of reduce f is also the ordinary remainder
f % g, exposing the algebraic view used by congruence lemmas.
Polynomial congruence modulo the defining quotient polynomial.
Equations
- Hex.FpPoly.Quotient.Congr f h = Hex.DensePoly.Congr f h g
Instances For
Congruent polynomials have the same canonical quotient representative.
Equal canonical quotient representatives imply congruence modulo the defining polynomial.
Equality of reduced representatives is equivalent to congruence modulo the quotient modulus.
All canonical quotient representatives, enumerated via bounded-degree polynomials.
Equations
Instances For
elements enumerates exactly p ^ deg g canonical representatives;
the order of the quotient ring FpPoly p / g.
Every quotient element appears in elements.
The quotient enumeration has no duplicate elements.
The quotient has p ^ deg(g) canonical representatives in the executable
list-cardinality sense.
Equality of quotient elements is equality of canonical remainders.
Zero in the quotient.
Equations
Instances For
Equations
The nonzero quotient elements, as a concrete duplicate-free sublist of
elements.
Equations
- Hex.FpPoly.Quotient.Internal.nonzeroElements = List.filter (fun (a : g.Quotient hmonic hg_pos) => decide (a ≠ 0)) Hex.FpPoly.Quotient.Internal.elements
Instances For
Membership in nonzeroElements is exactly nonzero quotient membership.
The nonzero quotient enumeration has no duplicates.
There are p ^ deg(g) - 1 nonzero quotient representatives.
One in the quotient.
Equations
Instances For
Equations
The class of the polynomial indeterminate.
Instances For
Addition of canonical quotient representatives.
Instances For
Equations
Negation of canonical quotient representatives.
Equations
- a.neg = Hex.FpPoly.Quotient.reduce (-a.val)
Instances For
Equations
Subtraction of canonical quotient representatives.
Instances For
Equations
Multiplication of canonical quotient representatives.
Instances For
Equations
Natural-number powers in the quotient.
Instances For
Equations
The stored representative of quotient zero is the reduction of the zero polynomial.
The stored representative of quotient one is the reduction of the constant
polynomial 1.
The stored representative of the quotient indeterminate is the reduced polynomial variable.
Addition of quotient elements reduces the sum of their canonical representatives.
Negation of a quotient element reduces the negated representative.
Subtraction of quotient elements reduces the difference of their canonical representatives.
Multiplication of quotient elements reduces the product of their canonical representatives.
Zeroth quotient power is the multiplicative identity.
Successor quotient powers multiply one more copy on the right.
Reducing a sum agrees with summing the separately reduced representatives and reducing once more.
Reducing a product agrees with multiplying the separately reduced representatives and reducing once more.
Reduction into the quotient preserves addition.
Reduction into the quotient preserves multiplication.
Reducing an already-canonical quotient representative leaves it unchanged.
The canonical quotient representative of 1 is the polynomial 1.
1 is a left identity for quotient multiplication.
1 is a right identity for quotient multiplication.
Quotient multiplication is associative.
Quotient multiplication is commutative.
Quotient powers turn addition of exponents into multiplication.
Quotient powers turn multiplication of exponents into iterated powering.
Reducing an executable polynomial power agrees with powering its quotient class.
The quotient class of the monomial c * X^n is the constant class c
times the nth power of the quotient indeterminate.
0 is a right identity for addition in the quotient ring.
0 is a left identity for addition in the quotient ring.
Quotient addition is associative. Together with add_zero, zero_add,
add_comm and add_left_neg this supplies the additive-group axioms behind the
Field (Quotient g hmonic hg_pos) instance.
Quotient addition is commutative.
Adding a quotient element to its left additive inverse gives zero.
Adding the right additive inverse of a quotient element gives zero.
Quotient subtraction is addition of the right additive inverse.
Subtracting a quotient element from itself gives zero.
A quotient subtraction is zero exactly when its left and right terms are equal.
Distinct quotient elements have nonzero difference.
A nonzero quotient difference witnesses distinct quotient elements.
Subtracting zero leaves a quotient element unchanged.
Quotient multiplication distributes over addition on the left.
Quotient multiplication distributes over addition on the right.
The xgcd-based inverse candidate, normalized by the leading coefficient of the computed gcd.
Equations
Instances For
Narrow Euclidean obligation for quotient inversion.
For a nonzero canonical representative modulo a monic irreducible positive-degree
polynomial, the normalized left Bezout coefficient is a multiplicative inverse
modulo g.
Multiplicative inverse candidate in the quotient, with the conventional
junk value 0⁻¹ = 0. The cancellation theorem below requires irreducibility.
Equations
- a.inv = if a.val = 0 then 0 else Hex.FpPoly.Quotient.reduce (Hex.FpPoly.Quotient.inverseCandidate a.val)
Instances For
Equations
The inverse of 0 is 0, the conventional junk value fixed by inv. This
is the inv_zero field axiom required by Field; it holds unconditionally and,
unlike mul_inv_cancel, needs no irreducibility hypothesis.
Multiplicative cancellation: when g is irreducible, every nonzero quotient
element a satisfies a * a⁻¹ = 1. This is the field-inverse axiom that
promotes Quotient g hmonic hg_pos from a commutative ring to a
Field; the
Hex.FpPoly.Irreducible hypothesis is
essential, since for reducible g a nonzero
zero-divisor has no inverse.
The inverse candidate also cancels on the left for nonzero quotient elements modulo an irreducible polynomial.
Multiplying any quotient element by zero gives zero.
Zero times any quotient element is zero.
Addition on the left by a fixed quotient element is cancellative.
Addition on the right by a fixed quotient element is cancellative.
If two quotient elements add to zero, the left element is the negative of the right element.
If two quotient elements add to zero, the right element is the negative of the left element.
Adding back the right-hand subtrahend cancels quotient subtraction.
Subtracting the right-hand addend cancels quotient addition.
Subtracting the left-hand addend cancels quotient addition.
Multiplication by a negated quotient element on the right negates the product.
Multiplication by a negated quotient element on the left negates the product.
Quotient multiplication distributes over subtraction on the left.
Quotient multiplication distributes over subtraction on the right.
Adjacent quotient subtractions cancel their shared middle term.