Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: General Weierstrass Equations


view this post on Zulip Email Gateway (Oct 01 2026 at 14:35):

From: Jasmin Blanchette <jasmin.blanchette@ifi.lmu.de>

Dear all,

I am happy to announce the first AFP entry I handled as an editor (with expert help from Tobias and René).

General Weierstrass Equations
by Arthur Freitas Ramos, David Barros Hulak, and Ruy Jose Guerra Barretto de Queiroz

This entry develops the general Weierstrass equation over commutative rings and fields. It defines the standard invariants, proves
y^2 + a_1xy + a_3y = x^3 + a_2x^2 + a_4x + a_6, formalizes the affine and projective equations and their singular points, and proves c_4^3 - c_6^2 = 1728\Delta over every field that the projective cubic is geometrically nonsingular exactly when \Delta \ne 0. Geometric singularities are taken over the algebraic closure, so the statement includes imperfect fields and characteristics 2 and 3. A final bridge specializes the development to the short equation and reuses the AFP Elliptic Curves Group Law entry. The definitions and invariant formulas follow the standard treatment in Silverman.

https://isa-afp.org/entries/General_Weierstrass.html

Enjoy!

Best,
Jasmin

smime.p7s


Last updated: Oct 08 2026 at 21:07 UTC