Commit 2024-07-25 07:50 d89cf7a1

View on Github →

Feat(RingTheory/Flat): add localization of flat module is flat (#15023) add that localization of a flat module is flat. This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

Estimated changes