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 101 research declarations. Search 10,000 more complete Mathlib declarations.
101 results
Clear filtersslashaction_generators'
Plain-language statement
If G is generated by a set s, then the slash action by elements in G is uniquely determined by the slash action by elements in s. See slashaction_generators for a version where s is a set of elements in SL(2, ℤ).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.inter_ball_encard_ge
Plain-language statement
This gives an upper bound on the number of points in the sphere packing X with norm less than R.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.inter_ball_encard_le
Plain-language statement
This gives an upper bound on the number of points in the sphere packing X with norm less than R.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.scale_density
Plain-language statement
Density of a scaled packing.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
SpherePacking.scale_finiteDensity
Plain-language statement
Finite density of a scaled packing.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
summable_pow_shift
Plain-language statement
Summability of (m+1)^k * exp(-2πm) via comparison with shifted sum.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.