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

Node Poly quadratic Twist Of map splits of residue

WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue

Plain-language statement

If the residues of (t', n') satisfy the trace and norm relations cut out by the node polynomial, then the node polynomial of the quadratic twist of the integral model by (t', n') splits over the residue field: the key identity φc₄ · φ(t'² - 4n') = -φc₆ (residue_c₄_mul_residue_eq_neg_c₆) reduces this to a square-class computation for residue charac...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Node Poly quadratic Twist Of map splits of residue of two eq zero

WeierstrassCurve.nodePoly_quadraticTwistOf_map_splits_of_residue_of_two_eq_zero

Plain-language statement

The residue characteristic 2 case of nodePoly_quadraticTwistOf_map_splits_of_residue: the Artin–Schreier split condition (nodePoly_map_splits_iff_of_two_eq_zero) holds with z = 0, because φ κ_W = 0. Indeed κ_W = D³κ - D²·n·a₁²·c₄ (kappa_quadraticTwistOf), and φκ = -φc₄·φn (hB), φa₁ = -φt' (hA), φD = φt'² (as 4 = 0), so `φκ_W = -φ...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Not exists smul quadratic Twist eq

WeierstrassCurve.not_exists_smul_quadraticTwist_eq

Plain-language statement

If j(E) ∉ {0, 1728} (so that the only automorphisms of E are ±1) then the quadratic twist is not isomorphic to E over K: twisting by L/K is a nontrivial operation. This can fail for j ∈ {0, 1728}: e.g. for E : y² = x³ + x of j-invariant 1728 over K = ℚ(i), the quadratic twist by any L = K(d^{1/2}) with d ∈ (K^×)⁴ ∖ (K^×)² is is...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Not Mem range algebra Map of residue not Mem

WeierstrassCurve.notMem_range_algebraMap_of_residue_notMem

Plain-language statement

If the residue of an integral element θ of S does not come from the residue field of R, then θ does not come from K either: an element of K integral over the integrally closed R lies in R, and residues are compatible.

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 of two ne zero

WeierstrassCurve.quadraticTwist_of_two_ne_zero

Plain-language statement

The classical formula for the quadratic twist away from characteristic 2. Suppose char K ≠ 2, so that after completing the square we may assume E has the form y² = x³ + a₂x² + a₄x + a₆, and suppose L = K(α) where α² = d is a nonsquare in K (every separable quadratic extension arises this way when char K ≠ 2). Then the quadratic twist of E...

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 galois

WeierstrassCurve.quadraticTwistPointEquiv_galois

Plain-language statement

Twisting the Galois action. The Galois action on the points of the quadratic twist is the Galois action on the points of E, twisted by the quadratic character of L/K: for σ ∈ Aut(M/K), transporting the action of σ on Eᴸ(M) through Eᴸ(M) ≅ E(M) gives χ(σ) times the action of σ on E(M). Taking M to be a separable closure of K, this...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record