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 research declarations. Search 10,000 more complete Mathlib declarations.
2569 results
TensorSpecies.unitTensor_eq_permT_dual
Plain-language statement
The unit tensor is symmetric on dualing the color.
Source project: Physlib
Person-level attribution pending.
Theory.small_satisfiable_of_consistent
Project documentation
Completeness theorem (I)
Source project: Foundation
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.