Cover Image

A Formalization of Divided Powers in Lean

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Chambert-Loir, Antoine, de Frutos-Fernández, María Inés
Format:	Preprint
Published:	2025
Subjects:	Logic in Computer Science Commutative Algebra 14F30 (Primary) 13J05 (Secondary)
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing Polynomial Laws and the Universal Divided Power Algebra
by: Chambert-Loir, Antoine, et al.
Published: (2025)

A Choice-free look at algebraic extensions of valuations
by: Aïd, Cédric
Published: (2025)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
by: Ramos, Arthur F., et al.
Published: (2026)

Projectable reduced $f$-rings admitting elimination of quantifiers
by: Guier, Jorge I.
Published: (2026)

Descending finite projective modules from a Novikov ring
by: Kim, Dongryul
Published: (2024)

On the recursive and explicit form of the general J.C.P. Miller formula with applications
by: Bugajewski, Dariusz, et al.
Published: (2023)

The reciprocal complement of a curve
by: Spirito, Dario
Published: (2025)

Threefolds of globally $F$-regular type with nef anti-canonical divisor
by: Cascini, Paolo, et al.
Published: (2024)

Pure subrings of Du Bois singularities are Du Bois singularities
by: Godfrey, Charles, et al.
Published: (2022)

Quasi-quadratic modules in pseudo-valuation domain
by: Fujita, Masato, et al.
Published: (2023)

Algebraic invariants of the special fiber ring of ladder determinantal modules
by: Costantini, Alessandra, et al.
Published: (2025)

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

When are permutation invariants Cohen-Macaulay?
by: Campbell, H. E. A., et al.
Published: (2023)

Invariants of toric double determinantal rings
by: Biermann, Jennifer, et al.
Published: (2025)

Normal reduction numbers for normal surface singularities with application to elliptic singularities of Brieskorn type
by: Okuma, Tomohiro, et al.
Published: (2018)

Puzzle Ideals for Grassmannians
by: Mou, Chenqi, et al.
Published: (2024)

On class groups of upper cluster algebras
by: Pompili, Mara
Published: (2023)

A variant of R{ö}hr's vanishing theorem with an application to the normal reduction number for normal surface singularities
by: Okuma, Tomohiro, et al.
Published: (2025)

Depth Sensitivity of Hilbert Coefficients
by: Nishida, Koji
Published: (2025)

On the Rees algebra and the conductor of an ideal
by: Gasanova, Oleksandra, et al.
Published: (2024)

The normal reduction number of two-dimensional cone-like singularities
by: Okuma, Tomohiro, et al.
Published: (2019)

Good ideals and $p_g$-ideals in two-dimensional normal singularities
by: Okuma, Tomohiro, et al.
Published: (2014)

Cohen-Macaulayness of powers of edge ideals of edge-weighted graphs
by: Li, Jiaxin, et al.
Published: (2025)

$F$-Invariants of Stanley-Reisner Rings
by: Badilla-Céspedes, Wágner
Published: (2020)

A note on the class of sober rings
by: Jafari, Saeid, et al.
Published: (2025)

Graded Injective Domains
by: Hensler, Mike, et al.
Published: (2025)

A Weaker Notion of Atomicity in Integral Domains
by: Benelmekki, Mohamed, et al.
Published: (2025)

On GL-domains and the ascent of the IDF property
by: Gonzalez, Victor, et al.
Published: (2025)

On the closed neighborhood ideal of the square of the path graph
by: Olteanu, Anda, et al.
Published: (2026)

Resolutions of Pinched Power Ideals
by: Đào, Hoài, et al.
Published: (2024)

Binomial edge rings associated to skew Ferrers diagrams
by: Lin, Kuei-Nuan, et al.
Published: (2025)

The multiplicity of cyclic coverings of a singularity of an algebraic variety
by: Kumagai, Toya, et al.
Published: (2024)

Binomial ideals attached to finite collections of cells
by: Herzog, Jürgen, et al.
Published: (2022)

Invariant Functions On Cluster Ensembles
by: Kaufman, Dani
Published: (2020)

Nearly Gorenstein normal graded rings
by: Okuma, Tomohiro, et al.
Published: (2026)

$F$-pure and $F$-injective singularities in equal characteristic zero
by: Yamaguchi, Tatsuki
Published: (2023)

The $v$-number of generalized binomial edge ideals of some graphs
by: Shen, Yi-Huang, et al.
Published: (2026)

Arithmetic properties encoded in undermonoids
by: Gotti, Felix, et al.
Published: (2024)

One-dimensional monoid algebras and ascending chains of principal ideals
by: Bu, Alan, et al.
Published: (2024)

Cohomology Vanishing theorems over some rings containing nilpotents
by: Puthenpurakal, Tony J.
Published: (2025)