Import Nagata's prime-generated factoriality theorem - #475

Open

Vilin97 wants to merge 28 commits into

mainfrom

codex/import42-nagatafactoriality

Commits on Sep 21, 2026

Import complete nagatafactoriality proof development
Vilin97
committed
00e156d
Advance nagatafactoriality port to Lean 4.34
Vilin97
committed
9fd9880
Complete Nagata Lean 4.34 port and local code checks
Vilin97
committed
2035cff

Commits on Sep 22, 2026

Merge remote-tracking branch 'origin/main' into pr-475
github-actions[bot]
committed
8e19209

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Merge remote-tracking branch 'origin/main' into pr-475
github-actions[bot]
committed
50e5070

Commits on Sep 25, 2026

Migrate Nagata factoriality to public modules
Vilin97
committed
a58605d
Sync current main for module checks
Vilin97
committed
595ddfa
Document Nagata proof provenance from upstream history
Vilin97
committed
6757e20
Merge current main while preserving the Nagata project card
Vilin97
committed
e1a6450
Reuse the localization-at-units equivalence in Nagata proofs
Vilin97
committed
08de88b
Merge remote-tracking branch 'origin/main' into HEAD
Vilin97
committed
e18e05a
Sync latest main for Nagata metadata validation
Vilin97
committed
f81fad5
Adopt concurrent Nagata main integration without losing reviewed repairs
Vilin97
committed
fe1cea3
Merge commit '0e9b057b62cc4eaa1b4a42cf23766cf7b9bd3537' into HEAD
Vilin97
committed
b1d25a4

Commits on Sep 26, 2026