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 14 research declarations. Search 10,000 more complete Mathlib declarations.
14 results
Clear filtersArkLib.Lattices.CyclotomicModulus.Xpow_natDegree
Plain-language statement
The key relation X^{2^α} = -1 (X^d = -1), proven via the quotient: X^d + 1 is the modulus, so it vanishes in the quotient.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Xpow_sub_one_isUnit
Plain-language statement
X^c - 1 is a unit whenever some X^{c·2^t} = -1. Then (∑_{j<2^t} (X^c)^j)·(X^c - 1) = (X^c)^{2^t} - 1 = -2, a unit (isUnit_two), so X^c - 1 is a unit. This is the crux of the trace-of-monomial vanishing (Hachi [NOZ26, §3, Claim 2]): it makes the geometric sum collapse without a domain.
Source project: ArkLib
Person-level attribution pending.