therefore
Sign up
Open navigation

Source-pinned research

Research proof index

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 1 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

1 result

Clear filters
Project-declaredLean 4.31.0

Trace H fixed of smul

ArkLib.Lattices.CyclotomicModulus.traceH_fixed_of_smul

Plain-language statement

If multiplication by g permutes Hexp (Hexp_generator_smul), then Ļƒ_g fixes Tr_H. The per-term step uses Ļƒ_g(Ļƒ_i a) = Ļƒ_{gĀ·i} a = Ļƒ_{(gĀ·i) mod 2^{Ī±+1}} a (composition + exponent-periodicity, both proven); the sum then reindexes along the permutation.

cryptographyproof systemscoding theory

Source project: ArkLib

Person-level attribution pending.

View proof record