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

1 topic

9 results

Clear filters

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

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

Δ base Change quadratic Twist Of ne zero

WeierstrassCurve.Δ_baseChange_quadraticTwistOf_ne_zero

Plain-language statement

The base change of the twisted integral model has nonzero discriminant: its Δ is (t'² - 4n')⁶ · Δ (Δ_quadraticTwistOf), and both factors are nonzero.

number theoryarithmetic geometryFermat's Last Theorem

Source project: Fermat's Last Theorem

Person-level attribution pending.

View proof record