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 423 research declarations. Search 10,000 more complete Mathlib declarations.
423 results
Clear filtersDomain.CosetFftDomainClass.toFinset_image_toFftDomain_eq_toFinset
Plain-language statement
Scaling the normalized FFT-domain image by ω 0 recovers the original coset FFT-domain image.
Source project: ArkLib
Person-level attribution pending.
Domain.FftDomainClass.domain_implies_char_ne_2
Plain-language statement
The existence of a nontrivial smooth FFT domain rules out characteristic 2.
Source project: ArkLib
Person-level attribution pending.
Domain.FftDomainClass.neg_one_mem_domain
Plain-language statement
In a smooth FFT domain of nonzero logarithmic size, -1 belongs to the domain.
Source project: ArkLib
Person-level attribution pending.
e_mul_R_div_R_sub_1_lt_e_add_1_real
Project documentation
This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...
Source project: ArkLib
Person-level attribution pending.
Fin.dappend_eq_addCases
Plain-language statement
dappend is equal to addCases. Marked as csimp to allow for switching to the addCases implementation during execution.
Source project: ArkLib
Person-level attribution pending.
Fin.drop_addCases_right
Plain-language statement
Dropping the first n + m elements of an addCases u v, where v is a n'-tuple and m ≤ n', is the same as dropping the first m elements of v.
Source project: ArkLib
Person-level attribution pending.