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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersArkLib.Lattices.CyclotomicModulus.mk_aeval_X_pow_periodic
Plain-language statement
(C-3 helper) aeval (X^n) and aeval (X^{n mod 2^{α+1}}) agree in the quotient.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.mk_monomial_coeff_full
Plain-language statement
Full coefficient of a (possibly high-degree) scaled monomial. For p < d, the p-th coefficient of the reduced c·X^m is (-1)^{m/d}·c at the folded position p = m mod d, and 0 elsewhere , the sign records how many times the exponent wrapped past X^d = -1.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.mk_monomial_coeff_lt
Plain-language statement
The j-th coefficient of the reduced c·X^i (for i < d) is c·[j = i].
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.mk_monomial_eq
Plain-language statement
The scaled monomial c·X^j ∈ Rq Φ factors as (constant c)·X^j.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.mk_reverse_eq_galoisAutₛ_mul
Plain-language statement
The reverse identity. In S = Z_q[X]/(X^{2^α}+1), the conjugation σ_{-1} (here the semantic automorphism galoisAutₛ of exponent conjExp = 2^{α+1}-1) and the polynomial reversal are related by mk(reverse p) = σ_{-1}(mk p) · (mk X)^{deg p}. This is the concrete handle behind "σ_{-1} swaps the two factors": since (mk X)^{deg p} is a unit, `σ...
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.mk_X_pow_conductor_eq_one
Plain-language statement
(C-1) X^{2^{α+1}} ≡ 1 in the quotient, since X^{2d} - 1 = (X^d - 1)(X^d + 1).
Source project: ArkLib
Person-level attribution pending.