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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 889 to 894 of 2,569 results.
Domain.CosetFftDomainClass.log_right_inverse'
Mathematical statement
Evaluating ω at the index found by log recovers x.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.mem_subdomain_of_le_of_mem_subdomain
Mathematical statement
If j ≤ i, then we do not have x ∈ subdomain ω i → x ∈ subdomain ω j in the general case but rescaling x as ω 0 ^ 2 ^ j * (ω 0)⁻¹ ^ 2 ^ i * x gives us a member of subdomain ω j.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.mul_mem_of_mem_toFftDomain_of_mem
Mathematical statement
Multiplying an element of the normalized FFT domain by an element of the original coset domain gives another element of the original coset domain.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.pow_mem_of_mem
Mathematical statement
If x lies in the jth subdomain, then x ^ 2 ^ i lies in the (j + i)th subdomain, provided j + i ≤ n.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.square_roots_explicit
Mathematical statement
The square roots of x inside the ith subdomain are exactly y and -y, for any square root y of x.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.subdomain_toFftDomain_comm
Mathematical statement
Normalizing the ith coset subdomain agrees with taking the ith FFT subdomain of the normalized domain.
Source project: ArkLib
Person-level attribution pending.