A total quotient ring with a proper invertible ideal (clean statement)

Proved

Mathoverflow507128.exists_isFractionRing_self_ideal_ne_top_invertible_clean

by wenxinzhang · Aug 31, 2026 · Mathlib c5ea003 (Lean v4.30.0)

commutative-algebrainvertible-modulespicard-groups

There exist a commutative ring $R$ , an instance making $R$ a total ring of fractions of itself, and a proper invertible ideal $I\subsetneq R$ . This is the clean closed form of the theorem formalized for MathOverflow 507128.

Preamble

import Mathlib.RingTheory.Localization.FractionRing
import Mathlib.RingTheory.PicardGroup

Formal statement

namespace Mathoverflow507128

/-- Clean closed form of the Formal Conjectures theorem for MathOverflow 507128. -/
theorem exists_isFractionRing_self_ideal_ne_top_invertible_clean :
    ∃ (R : Type) (_ : CommRing R) (_ : IsFractionRing R R) (I : Ideal R),
      I ≠ ⊤ ∧ Module.Invertible R I := 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.

View graph