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

1 topic

95 results

Clear filters
Project-declaredLean 4.32.0

Quadratic Twist Point Equiv map

WeierstrassCurve.quadraticTwistPointEquiv_map

Plain-language statement

Naturality of quadraticTwistPointEquiv in M: the isomorphisms on M-points over varying M ⊇ L are all induced by a single isomorphism of curves over L, so they commute with the maps on points induced by any L-algebra homomorphism.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Point Equiv map of not fixed

WeierstrassCurve.quadraticTwistPointEquiv_map_of_not_fixed

Plain-language statement

The anti-equivariance underlying quadraticTwistPointEquiv_galois: if σ ∈ Aut(M/K) does not fix L pointwise (χ(σ) = -1), then transporting its action through Eᴸ(M) ≅ E(M) gives minus its action. This is the point-level shadow of quadraticTwistVarChange_baseChange_map.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Var Change base Change map

WeierstrassCurve.quadraticTwistVarChange_baseChange_map

Plain-language statement

The M-level form of the twist's defining cocycle: any σ ∈ Aut(M/K) not fixing L pointwise (i.e. with χ(σ) = -1) conjugates the base change to M of quadraticTwistVarChange by the automorphism [-1] of E. This is the base change of quadraticTwistVarChange_map.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Quadratic Twist Var Change map

WeierstrassCurve.quadraticTwistVarChange_map

Plain-language statement

The defining cocycle of the quadratic twist. The nontrivial σ ∈ Gal(L/K) conjugates the change of variables quadraticTwistVarChange (carrying E to Eᴸ) by the automorphism [-1] of E. This is the datum expressing that Eᴸ is the descent of E along the twisted Galois action σ ↦ (-1) ∘ σ, and it holds for every j.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Residue c₄ mul residue eq neg c₆

WeierstrassCurve.residue_c₄_mul_residue_eq_neg_c₆

Plain-language statement

The key identity φc₄ · φ(t'² - 4n') = -φc₆ of the twisting datum (t', n'): if its residues satisfy the trace and norm relations cut out by the node polynomial (κ = 54 b₆ - 3 b₂ b₄ + a₂ c₄), then the discriminant identity splitPolynomial_discrim turns them into this identity.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Weierstrass Curve tate A₄ eq eval Int

WeierstrassCurve.tateA₄_eq_evalInt

Plain-language statement

The Lambert series rearrangement ∑_{n≥1} n³qⁿ/(1-qⁿ) = ∑_{n≥1} σ₃(n)qⁿ for |q| < 1: the defining series of tateA₄ is the evaluation of the formal series a₄(q) = -5s₃(q) ∈ ℤ⟦q⟧.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record