Annihilated nonunits make the idealization a total quotient ring

import Mathlib.Algebra.TrivSqZeroExt.Basic
import Mathlib.LinearAlgebra.TensorProduct.Prod
import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.RingTheory.PicardGroup
import Definitions.Def_RybinP18_CuspidalCubicInput
import Definitions.Def_RybinP18_MO507128

/-!
# MathOverflow 507128: the idealization step

This file deliberately does not import or clone `formal-conjectures`.  It copies the
statement of the target theorem and proves the square-zero idealization argument using
mathlib.

The input for the idealization is constructed explicitly from the cuspidal cubic
`Y² = X³`.  Thus the final `#print axioms` contains no problem-specific axiom.
-/

namespace Mathoverflow507128

universe u v

variable (D : Type u) [CommRing D]
variable (M : Type v) [AddCommGroup M] [Module D M]

local instance p2m_Theorems_Thm_Mathoverflow507128_isFractionRing_self_of_kills_nonunits_1 : Module Dᵐᵒᵖ M :=
  Module.compHom M ((RingHom.id D).fromOpposite mul_comm)

local instance p2m_Theorems_Thm_Mathoverflow507128_isFractionRing_self_of_kills_nonunits_2 : IsCentralScalar D M := ⟨fun _ _ => rfl⟩

local notation "R" => TrivSqZeroExt D M























/-- If every nonunit of `D` kills a nonzero element of `M`, every regular
element of `D ⋉ M` is a unit. -/
theorem isFractionRing_self_of_kills_nonunits
    (hkill : ∀ a : D, ¬ IsUnit a → ∃ m : M, m ≠ 0 ∧ a • m = 0) :
    IsFractionRing R R := by
  sorry











end Mathoverflow507128

namespace Mathoverflow507128



end Mathoverflow507128