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 121 research declarations. Search 10,000 more complete Mathlib declarations.

1 topic

121 results

Clear filters
Project-declaredLean 4.33.0-rc1

Tate Theorem lemma 2

Rep.split.TateTheorem_lemma_2

Plain-language statement

For any subgroup H of G, the connecting hommorphism in the splitting module long exact sequence H¹(H,aug) ⟶ H²(H,M) is an isomorphism.

number theoryclass field theorylocal fields

Source project: Class Field Theory

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Τ property

Rep.split.τ_property

Plain-language statement

Given a 2-cocycle σ, the image of σ in the splitting module of σ is equal to the coboundary of τ σ.

number theoryclass field theorylocal fields

Source project: Class Field Theory

Person-level attribution pending.

View proof record
Project-declaredLean 4.33.0-rc1

Trivial Tate Cohomology of cases

Rep.TrivialTateCohomology.of_cases

Plain-language statement

To check that a finite group has trivial Tate cohomology, it's enough to show it has trivial cohomology and trivial homology, and that the 0-th and -1st Tate cohomology groups are trivial.

number theoryclass field theorylocal fields

Source project: Class Field Theory

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Analytic weierstrass

TateCurve.Blueprint.analytic_weierstrass

Project documentation

The analytic form of the main theorem (Silverman, Advanced topics, Theorem V.1.1(a)): for 0 < ‖q‖ < ‖u‖ < 1, Yₐ² + XₐYₐ = Xₐ³ - 5s₃(q)Xₐ - (5s₃(q) + 7s₅(q))/12. Proof sketch: the hypotheses ensure u ∉ qᶻ, and we may choose z, τ with e z = u, e τ = q, 0 < im z < im τ (so z ∉ Λ_τ). Substitute the four q-expansions into the differential...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Deriv Weierstrass P q expansion

TateCurve.Blueprint.derivWeierstrassP_q_expansion

Plain-language statement

The q-expansion of ℘' (Silverman, Advanced topics, Theorem I.6.2): under the hypotheses of weierstrassP_q_expansion, ℘'(z; Λ_τ) = (2πi)³ (Xₐ(e z, e τ) + 2Yₐ(e z, e τ)). Proof: as for weierstrassP_q_expansion, but simpler: group the absolutely convergent sum ℘'(z) = -2∑_ω (z - ω)⁻³ into rows ω = nτ + m (no regularising terms are needed here...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Eq zero of forall has Sum zero

TateCurve.Blueprint.eq_zero_of_forall_hasSum_zero

Project documentation

The descent lemma: a formal power series F ∈ ℚ(u)⟦q⟧ vanishes provided that, for infinitely many u₀ : ℂ, the evaluated series ∑ₙ Fₙ(u₀)q₀ⁿ converges with sum 0 for all sufficiently small nonzero q₀. Proof sketch: fix u₀. The function q₀ ↦ ∑ₙ Fₙ(u₀)q₀ⁿ is analytic on ‖q₀‖ < r (a power series converging pointwise on a disc is analytic there)...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record