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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersadiabatic_relation_log
Plain-language statement
Adiabatic relation in logarithmic form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then c * log (Ua/Ub) + log (Va/Vb) = 0.
Source project: Physlib
Person-level attribution pending.
adiabatic_relation_UaUbVaVb
Plain-language statement
Adiabatic relation in product form: If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then (Ua/Ub)^c * (Va/Vb) = 1.
Source project: Physlib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.gadgetDecompose_lawful
Plain-language statement
The base-b gadget decomposition is a lawful gadget decomposition.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.gadgetEntry_finProdFinEquiv
Plain-language statement
The gadget entry at the flattened index finProdFinEquiv (i', e) is constRq (base^e) on the diagonal block and 0 elsewhere.
Source project: ArkLib
Person-level attribution pending.
ArkLib.Lattices.Ajtai.gadgetMul_apply
Plain-language statement
The gadget product, evaluated at row i, is the base-weighted sum of the digits slots of block i.
Source project: ArkLib
Person-level attribution pending.
ArkLib.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.