Mul conj Exp mod
ArkLib.Lattices.CyclotomicModulus.mul_conjExp_mod
Plain-language statement
The conjugate σ_{-1}(X^e) lands at position d - e (mod d), for 0 < e < d.
Source project: ArkLib
Person-level attribution pending.
Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 14 research declarations. Search 10,000 more complete Mathlib declarations.
14 results
Clear filtersArkLib.Lattices.CyclotomicModulus.mul_conjExp_mod
Plain-language statement
The conjugate σ_{-1}(X^e) lands at position d - e (mod d), for 0 < e < d.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.vElt_coeff
Plain-language statement
Coefficient of the basis element: v_j has coefficient [s = j]·(2 if j=0 else 1) at the position (d/2k)·s. The two basis exponents of v_j are (d/2k)·j (degree < d/2) and its conjugate (degree > d/2); only the former can equal (d/2k)·s < d/2, except at j=0 where the conjugate coincides (giving the doubling).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.vElt_coeff_full
Plain-language statement
Full coefficient formula for the basis element v_j. For every position p < d, the p-th coefficient of v_j = X^{(d/2k)·j} + σ_{-1}(X^{(d/2k)·j}) is: 2 at p = 0 when j = 0; otherwise +1 at p = (d/2k)·j, -1 at the complementary position p = d - (d/2k)·j, and 0 elsewhere. This extends vElt_coeff (which only covers the positions `...
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Xpow_coeff_of_lt
Plain-language statement
For i < 2^α (below the modulus degree), X^i is already reduced, so its j-th coefficient is the Kronecker delta [j = i].
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Xpow_mul_coeff
Plain-language statement
Coefficient of an X^e-shift of a reduced element. For e < d, p < d and any x : R_q, the p-th coefficient of x·X^e is the (p-e)-th coefficient of x (no wrap, e ≤ p), or minus the (p+d-e)-th coefficient (one wrap past X^d = -1, p < e). This is the only place the proof needs the ring's multiplication; everything downstream is coef...
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Xpow_mul_conjExp
Plain-language statement
Conjugation negates a square-root-of--1 monomial: if X^{2j} = -1 then σ_{-1}(X^j) = X^{j·conjExp} = -X^j. The exponent j·conjExp ≡ -j, so X^{j·conjExp} is the inverse of X^j; and X^j·(-X^j) = -(X^j)² = -X^{2j} = 1, so the inverse is -X^j.
Source project: ArkLib
Person-level attribution pending.