TY  - RPRT
TI  - Formalization in Lean of faithfully flat descent of projectivity
AU  - Liran Shaul
PY  - 2026
UR  - https://arxiv.org/abs/2603.04376
ID  - 2603.04376
ER  -