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 35 research declarations. Search 10,000 more complete Mathlib declarations.
35 results
Clear filtersserre_D_slash_equivariant
Plain-language statement
Serre derivative is equivariant under the slash action. More precisely, if F is invariant under the slash action of weight k, then serre_D k F is invariant under the slash action of weight k + 2.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
theta_g_S_action
Plain-language statement
g is invariant under S. Proof: g = (2H₂ + H₄)f₂ + (H₂ + 2H₄)f₄ Under S: H₂ ↦ -H₄, H₄ ↦ -H₂, f₂ ↦ -f₄, f₄ ↦ -f₂ g|S = (2(-H₄) + (-H₂))(-f₄) + ((-H₄) + 2(-H₂))(-f₂) = (2H₄ + H₂)f₄ + (H₄ + 2H₂)f₂ = g
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
theta_g_T_action
Plain-language statement
g is invariant under T. Proof: Under T: H₂ ↦ -H₂, H₄ ↦ H₃, f₂ ↦ -f₂, f₄ ↦ f₃ = f₂ + f₄ g|T = (2(-H₂) + H₃)(-f₂) + ((-H₂) + 2H₃)(f₂ + f₄) Using Jacobi: H₃ = H₂ + H₄, simplifies to g.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
theta_h_S_action
Plain-language statement
h is invariant under S. Proof: h = f₂² + f₂f₄ + f₄² Under S: f₂|[4]S = -f₄, f₄|[4]S = -f₂ Using mul_slash_SL2: (f₂²)|[8]S = (f₂|[4]S)² = (-f₄)² = f₄² (f₂f₄)|[8]S = (f₂|[4]S)(f₄|[4]S) = (-f₄)(-f₂) = f₂f₄ (f₄²)|[8]S = (f₄|[4]S)² = (-f₂)² = f₂² So h|[8]S = f₄² + f₂f₄ + f₂² = f₂² + f₂f₄ + f₄² = h
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
theta_h_T_action
Plain-language statement
h is invariant under T. Proof: Under T: f₂ ↦ -f₂, f₄ ↦ f₃ = f₂ + f₄ h|T = (-f₂)² + (-f₂)(f₂ + f₄) + (f₂ + f₄)² = f₂² - f₂² - f₂f₄ + f₂² + 2f₂f₄ + f₄² = f₂² + f₂f₄ + f₄² = h
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.