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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersArkLib.Lattices.CyclotomicModulus.quotientHom_reduce
Plain-language statement
Reduction modulo φ is invisible in the quotient: reduce p ≡ p (mod φ). This is the cyclotomic analogue of the NegacyclicRingSemantics soundness data.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.coeff_eq_zero_of_natDegree_le
Plain-language statement
A reduced representative has zero coefficients at and beyond deg φ.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.constRq_mul_coeff
Plain-language statement
Multiplying by the constant constRq Φ c scales coefficients by c.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.constRq_val
Plain-language statement
The constant constRq Φ c has underlying polynomial C c (no reduction occurs, as deg (C c) = 0 < deg φ).
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.eq_zero_of_l1Norm_eq_zero
Plain-language statement
A ring element with zero centered ℓ₁ norm is 0: every centered coefficient representative below deg φ vanishes (ZMod.valMinAbs_eq_zero), and the representative is reduced (degree < deg φ), so the underlying polynomial is 0.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.CyclotomicModulus.Rq.eq_zero_of_l2NormSq_eq_zero
Plain-language statement
A ring element with zero centered squared ℓ₂ norm is 0: every centered coefficient representative below deg φ vanishes (ZMod.valMinAbs_eq_zero), and the representative is reduced (degree < deg φ), so the underlying polynomial is 0.
Source project: ArkLib
Person-level attribution pending.