@misc{indiciae734330411ded, title = {Formalization in Lean of faithfully flat descent of projectivity}, author = {Liran Shaul}, year = {2026}, url = {https://arxiv.org/abs/2603.04376}, note = {Source identifier: 2603.04376} }