Cover Image

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Ramos, Arthur F., de Queiroz, Ruy J. G. B., de Oliveira, Anjolina G.
Format:	Preprint
Published:	2026
Subjects:	Commutative Algebra Logic in Computer Science 03B35, 13A05, 13B30
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Azumaya algebras and Barr Theorem
by: Coquand, Thierry, et al.
Published: (2023)

A special subring of the Nagata ring and the Serre's conjecture ring
by: Baek, Hyungtae, et al.
Published: (2024)

On extensions of Cohen Structure Theorem
by: Caviglia, Elena, et al.
Published: (2025)

A Formalization of Divided Powers in Lean
by: Chambert-Loir, Antoine, et al.
Published: (2025)

The Briançon-Skoda Theorem via weak functoriality of big Cohen-Macaulay algebras
by: Rodríguez-Villalobos, Sandra, et al.
Published: (2024)

New Results On $S-r-$ideals in Commutative Rings
by: Gündüz, Abuzer, et al.
Published: (2025)

$L$-smooth factorization for Noetherian $F$-finite rings
by: Blickle, Manuel, et al.
Published: (2025)

Decidability for the theory of modules over a Prüfer domain
by: Gregory, Lorna
Published: (2021)

On the behavior of $F$-thresholds with respect to the fibers of blow-ups and $F$-rationality
by: FakhriVaighan, Ghazaleh
Published: (2025)

Relative Inverse Limit Perfection of Derived Commutative Rings
by: Fink, Daniel
Published: (2025)

The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
by: Ramos, Arthur F., et al.
Published: (2025)

On the transfer of certain ring-theoretic properties in Anderson rings
by: Baek, Hyungtae, et al.
Published: (2024)

Semi-fiber products of algebras and lifting of complexes
by: Nasseh, Saeed, et al.
Published: (2026)

Cardinality of groups and rings via the idempotency of infinite cardinals
by: Tarizadeh, Abolfazl
Published: (2024)

Endogenies and Linearisation
by: Deloro, Adrien, et al.
Published: (2024)

André-Quillen homology and ascent of complete intersection flat dimensions
by: Sather-Wagstaff, Keri Ann, et al.
Published: (2025)

Unmixedness of generalized Veronese bi-type ideals
by: La Barbiera, Monica, et al.
Published: (2024)

$F$-Volumes
by: Badilla-Céspedes, Wágner, et al.
Published: (2019)

On strongly multiplicative sets
by: Koç, Suat
Published: (2025)

Analytic Ax-Kochen-Ersov theory with lifts of the residue field and value group
by: Bhardwaj, Neer, et al.
Published: (2024)

Trace ideals, conductors, and ideals of finite (phantom) projective dimension
by: Kimura, Kaito
Published: (2025)

Homological properties of the relative Frobenius morphism
by: McDonald, Peter M.
Published: (2024)

Straightening laws for Chow rings of matroids
by: Larson, Matt
Published: (2024)

On vanishing of higher direct images of the structure sheaf
by: Ishii, Shihoko, et al.
Published: (2024)

On Partial Trace Ideals
by: Dey, Souvik, et al.
Published: (2026)

On $w$-Hilbert domains
by: Baek, Hyungtae
Published: (2026)

Formalizing Computational Paths and Fundamental Groups in Lean
by: Ramos, Arthur F., et al.
Published: (2025)

Tame and wild primes in direct products of commutative rings
by: Tarizadeh, Abolfazl, et al.
Published: (2022)

Bounds for the Hilbert-Kunz Multiplicity of Singular Rings
by: Aberbach, Ian M., et al.
Published: (2024)

Note on length and multiplicity of modules over two-dimensional regular local rings
by: Hayasaka, Futoshi, et al.
Published: (2025)

Splitting in a complete local ring and decomposition its group of units
by: Tarizadeh, Abolfazl
Published: (2025)

Combinatorial properties of strong quasi-n-partite graphs
by: La Barbiera, Monica, et al.
Published: (2024)

Homogeneous ideals with minimal singularity thresholds
by: Baily, Benjamin
Published: (2026)

Blow-up rings and $F$-rationality
by: Kotal, Nirmal, et al.
Published: (2023)

The non-$F$-rational locus of Rees algebras
by: Kotal, Nirmal, et al.
Published: (2023)

Rees algebras and $p_g$-ideals in a two-dimensional normal local domain
by: Okuma, Tomohiro, et al.
Published: (2015)

Hilbert polynomials for finitary matroids
by: Fornasiero, Antongiulio, et al.
Published: (2022)

SAT Solving Using XOR-OR-AND Normal Forms
by: Andraschko, Bernhard, et al.
Published: (2023)

F-Splittings of seminormal monoid algebras
by: Hering, Milena, et al.
Published: (2025)

On Stability and Denominators of F-pure thresholds in Families of Diagonal Hypersurfaces
by: Chua, Gari Lincoln
Published: (2024)