PR !4#12438: feat: some APIs for flat modules

Stream: triage

[Random Issue Bot]

Today I chose PR 12438 for discussion!

feat: some APIs for flat modules
Created by Jujian Zhang (@jjaassoonn) on 2024-04-26
Labels: WIP, merge-conflict, t-category-theory

Is this PR still relevant? Any recent updates? Anyone making progress?

[Johan Commelin]

Is this still stuck on the horseshoe lemma? We had that in LTE? Could be a nice project to move it to mathlib