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 8 research declarations. Search 10,000 more complete Mathlib declarations.
8 results
Clear filtersArkLib.Lattices.CyclotomicModulus.dvd_cyclotomic_factor
Plain-language statement
X^(2^(α-1)) - C r divides X^(2^α)+1 when r^2 = -1 and α ≥ 1.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.emultiplicity_two_q_pow_sub_one
Plain-language statement
The 2-adic valuation of q^(2^k) - 1 is k + 2.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.emultiplicity_two_q_sub_one
Plain-language statement
For a prime q with q % 8 = 5, q - 1 ≡ 4 (mod 8), hence v₂(q-1) = 2.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.halfSum_coeff_eq_zero
Plain-language statement
Linear independence of 1, ζ, …, ζ^{2^{α-1}-1} makes each collected coefficient vanish.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.irreducible_X_pow_sub_C_r
Plain-language statement
Irreducibility of the splitting factor. X^{2^{α-1}} - r is irreducible over ZMod q, given the order fact horder (supplied by orderOf_q_mod_two_pow). Uses ZMod.irreducible_of_dvd_cyclotomic_of_natDegree: the factor divides cyclotomic 2^{α+1} = X^{2^α}+1 and has degree 2^{α-1} = orderOf (q mod 2^{α+1}).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.orderOf_q_mod_two_pow
Plain-language statement
The multiplicative order of q modulo 2^(α+1) is 2^(α-1), phrased to match ZMod.irreducible_of_dvd_cyclotomic_of_natDegree (K = ZMod q, n = 2^(α+1)).
Source project: ArkLib
Person-level attribution pending.