WIP: import Stafford 3.8 - #503

Open

Vilin97 wants to merge 48 commits into

mainfrom

codex/import42-stafford38-formal

Commits on Sep 21, 2026

Import Stafford 3.8
Vilin97
committed
ba7bb7c
Refine full import for Lean 4.34 compatibility and quality checks
Vilin97
committed
b167fca
Update polynomial coefficients and finite-length transport APIs
Vilin97
committed
8c8b8ed
Port Stafford algebra APIs and generalize the Euler-subring factorization
Vilin97
committed
91d1d93
Update remaining Stafford coefficient APIs and isolate scalar inference
Vilin97
committed
e90a50b
Port Stafford Euler, quotient and retained-place constructions
Vilin97
committed
28c550d
Make localized page and coordinate-ring instances explicit
Vilin97
committed
67e4e89
Port retained projective equation and ground-map transport
Vilin97
committed
fcc3992
Complete retained divisor frame port to current Mathlib
Vilin97
committed
0e36f11
Narrow Stafford38 imports and remove inherited linter waivers
Vilin97
committed
15cab3c
Use ordinary proof-local instances and isolate algebraic field extension
Vilin97
committed
6f48e50
Document Stafford APIs and normalize the filtered page proofs
Vilin97
committed
9bbd60c
Finish Stafford documentation and generalize page action constructions
Vilin97
committed
3d9bc63
Complete Stafford quality checks and precise field assumptions
Vilin97
committed
b00f1d7
Keep localization commutators independent of Lie product imports
Vilin97
committed
987700c

Commits on Sep 22, 2026

Merge remote-tracking branch 'origin/main' into pr-503
github-actions[bot]
committed
b862ca2

Commits on Sep 23, 2026

Commits on Sep 24, 2026

Merge remote-tracking branch 'origin/main' into pr-503
github-actions[bot]
committed
31d2031

Commits on Sep 25, 2026

Commits on Sep 26, 2026