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 3 research declarations. Search 10,000 more complete Mathlib declarations.
3 results
Clear filtersArkLib.Lattices.CyclotomicModulus.card_fixedSubring_le
Plain-language statement
|R_q^H| ≤ q^k, from ψ : (R_q^H)^{d/k} ↪ R_q injective and |R_q| = q^{2^α}: |R_q^H|^{d/k} ≤ q^{2^α} = (q^k)^{d/k}.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.fixedBasisMap_injective
Plain-language statement
fixedBasisMap is injective: distinct coefficient vectors give distinct fixed elements, read off at coefficient position (d/2k)·s via vElt_coeff and cancellation of the unit 2 if s=0 else 1.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.fixedSubring_coeff_eq_zero
Plain-language statement
Support of a fixed element (Eq. 7). Every x ∈ R_q^H has its nonzero coefficients on multiples of d/2k = 2^{α-κ-1}: for p < d with 2^{α-κ-1} ∤ p, x.1.coeff p = 0. This comes from the symmetric vElt basis (fixedBasisMap is surjective by card_fixedSubring_eq), each of whose elements is supported , by vElt_coeff_full , on the two multipl...
Source project: ArkLib
Person-level attribution pending.