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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersArkLib.Lattices.CyclotomicModulus.galoisAut_map_one
Plain-language statement
σ_i fixes 1, since only the constant term contributes (so in particular σ_1 fixes it).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.galoisAut_mul
Plain-language statement
Multiplicativity of the computable automorphism, transported from galoisAutₛ (a RingHom) through the soundness bridge.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.galoisAut_sum_toPoly_eq_aeval
Plain-language statement
(S5) The core polynomial identity behind soundness: the monomial-remapped sum (before reduction) equals aeval (X^i) of the underlying polynomial. Both sides are ∑_{k<d} X^{ki}·a_k.
Source project: ArkLib
Person-level attribution pending.
ArkLib.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_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.
ArkLib.Lattices.CyclotomicModulus.powTwo_galoisAeval_mem
Plain-language statement
Well-definedness on the power-of-two ring: aeval (X^i) maps the modulus ideal into itself for odd i, since X^{2^α} + 1 ∣ (X^{2^α})^i + 1.
Source project: ArkLib
Person-level attribution pending.