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

Delta imag axis real

Delta_imag_axis_real

Project documentation

Ī” transforms under S as: Ī”(-1/z) = zĀ¹Ā² Ā· Ī”(z) -/ lemma Ī”_S_transform (z : ā„) : Ī” (ModularGroup.S ā€¢ z) = z ^ (12 : ā„•) * Ī” z := by have h := Discriminant_S_invariant simp only [funext_iff] at h specialize h z rw [SL_slash_apply] at h simp only [ModularGroup.denom_S, zpow_neg] at h field_simp [ne_zero z] at h rw [h, mul_comm] theorem Delta_boundedfactor : Te...

sphere packingFourier analysismodular forms

Source project: Sphere Packing in Dimension 8

Person-level attribution pending.

View proof record