Clean explicit idealization input from the cuspidal cubic
ProvedMathoverflow507128.idealizationInput_explicit_cleancommutative-algebrainvertible-modulespicard-groups
The cuspidal cubic supplies explicit commutative-ring, module, and ideal data satisfying the three inputs needed by the idealization argument: a proper invertible ideal, injective tensor multiplication, and a nonzero module element annihilated by every nonunit.
Preamble
import Definitions.Def_RybinP18_CuspidalCubicInput import Definitions.Def_RybinP18_MO507128
Formal statement
namespace Mathoverflow507128 /-- Platform-safe closed statement of the explicit cuspidal-cubic idealization input. -/ theorem idealizationInput_explicit_clean : IdealizationInput := by sorry end Mathoverflow507128
Source
CUHK-Shenzhen AI Math Problem 18, https://rybindmitry.github.io/problems/18.html. Lean formalization by Patricia Purtill and Kenta Kitamura, discussed at https://github.com/google-deepmind/formal-conjectures/pull/4644#issuecomment-5089566133; staged from Kenta Kitamura's Apache-2.0 repository https://github.com/KitaKen1/mo507128-lean at commit e9507429c01c4288089e4af1c92a03b7d1e17f74.