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.emultiplicity_four_pow_sub_one
Plain-language statement
2-adic LTE for g = 4·2^κ + 1: v₂(gⁿ − 1) = (κ+2) + v₂(n).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.four_pow_mod_period
Plain-language statement
The power gⁿ mod 2^{α+1} depends only on n mod 2^{α-κ-1} (period = order of g).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.two_pow_dvd_four_pow_sub_one_iff
Plain-language statement
Divisibility characterization: 2^{α+1} ∣ gⁿ − 1 ↔ 2^{α-κ-1} ∣ n for g = 4·2^κ+1, when κ + 1 ≤ α (so α - κ - 1 is the genuine order d/(2k)).
Source project: ArkLib
Person-level attribution pending.