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 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,045 to 1,050 of 2,569 results.
f₄_sq_mul_eq
Mathematical statement
Key algebraic identity for proving f₂ = f₄ = 0. Given Af₂ + Bf₄ = 0, we have f₄² * (A² - AB + B²) = A² * (f₂² + f₂f₄ + f₄²).
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₄_T_action
Mathematical statement
f₄ transforms under T as f₄|T = f₃. Proof outline: 1. (serre_D 2 H₄)|[4]T = serre_D 2 (H₄|[2]T) = serre_D 2 H₃ 2. (H₄(2H₂ + H₄))|[4]T = H₃(2(-H₂) + H₃) = H₃(H₃ - 2H₂) Using Jacobi H₃ = H₂ + H₄: H₃ - 2H₂ = H₄ - H₂ 3. f₄|[4]T = serre_D 2 H₃ + (1/6)H₃(H₃ - 2H₂) But H₂² - H₄² = (H₂ - H₄)(H₂ + H₄) = (H₂ - H₄)H₃ So (1/6)(H₂² - H₄²) = -(1/6)H₃(H₄ - H₂) = -(1/6)H...
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
f₄_tendsto_atImInfty
Mathematical statement
f₄ tends to 0 at infinity. Proof: f₄ = serre_D 2 H₄ + (1/6)H₄(2H₂ + H₄) serre_D 2 H₄ = D H₄ - (1/6)E₂ H₄ → 0 - (1/6)11 = -1/6 (since H₄ → 1, E₂ → 1) H₄(2H₂ + H₄) → 1*(0 + 1) = 1 So f₄ → -1/6 + (1/6)*1 = 0.
Source project: Sphere Packing in Dimension 8
Person-level attribution pending.
FderivCcinfty
Mathematical statement
The Fréchet derivative x ↦ (∂ˢψ(x))(unitSeq s) of a test function ψ ∈ Cc^∞(U) again lies in Cc^∞(U). This is used to compose the weak derivative definition with itself.
Source project: PDE
Person-level attribution pending.
FermatLastTheorem.of_p_ge_5
Mathematical statement
If Fermat's Last Theorem is true for primes p ≥ 5, then FLT is true.
Source project: Fermat's Last Theorem
Person-level attribution pending.
Fermion.comm_metricRaw
Mathematical statement
Multiplying an element of SL(2, ℂ) on the left with the metric 𝓔 is equivalent to multiplying the inverse-transpose of that element on the right with the metric.
Source project: Physlib
Person-level attribution pending.