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.32.0

Exists smul base Change and map eq

WeierstrassCurve.exists_smul_baseChange_and_map_eq

Plain-language statement

An explicit L-isomorphism (Eᶿ)ᴸ ≅ Eᴸ (the change of variables of the module docstring) which moreover is anti-equivariant for the Galois action: its conjugate by the nontrivial σ ∈ Gal(L/K) differs from it by the automorphism [-1] of E. This nontrivial cocycle is the origin of the twist being a nontrivial form 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

Exists smul eq or exists smul eq quadratic Twist

WeierstrassCurve.exists_smul_eq_or_exists_smul_eq_quadraticTwist

Plain-language statement

Classification of the forms of E split by L/K, for j(E) ∉ {0, 1728}: an elliptic curve over K which becomes isomorphic to E over L is isomorphic over K either to E or to its quadratic twist by L. (Such forms are classified by H¹(Gal(L/K), Aut(E_L)) = Hom(ℤ/2, {±1}), which has order 2. For j ∈ {0, 1728} the automorphism group is large...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Exists smul quadratic Twist base Change eq

WeierstrassCurve.exists_smul_quadraticTwist_baseChange_eq

Plain-language statement

The quadratic twist becomes isomorphic to E after base change to L. (Over a field, isomorphisms of Weierstrass curves are exactly the admissible changes of variables WeierstrassCurve.VariableChange, acting via .) The point-level consequences of this isomorphism, which is what most applications need, are recorded separately in `quadraticTwistPoint...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Has Multiplicative Reduction base Change quadratic Twist Of

WeierstrassCurve.hasMultiplicativeReduction_baseChange_quadraticTwistOf

Plain-language statement

The twist by a unit discriminant keeps multiplicative reduction. If E has multiplicative reduction and D = t² - 4n is a unit of R (residue ≠ 0), then the base change of the R-model twist (E.integralModel R).quadraticTwistOf t n again has multiplicative reduction: its c₄ = D² · c₄ is a unit (so the model is minimal and the reduction multi...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Has Split Multiplicative Reduction quadratic Twist Of of residue

WeierstrassCurve.hasSplitMultiplicativeReduction_quadraticTwistOf_of_residue

Plain-language statement

Packaging nodePoly_quadraticTwistOf_map_splits_of_residue: if the base change of the twisted integral model has multiplicative reduction and the residues of (t', n') satisfy the trace and norm relations, then the reduction is split multiplicative.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record
Project-declaredLean 4.32.0

Integral Model base Change map

WeierstrassCurve.integralModel_baseChange_map

Plain-language statement

The integral model of the base change is the base change of the integral model. Both sides are lifts of E.baseChange l along the injective map 𝒪[l] → l (injectivity from IsFractionRing), and lifts along an injective map are unique: compare coefficientwise via integralModel_a₁_eq on both sides and the commuting square algebraMap_integerMap. (O...

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record