Theorem Module.free_of_flat_of_finrank_eq

Modification history

2025-11-04 08:07
Mathlib/RingTheory/LocalRing/Module.lean
feat(RingTheory): finite flat constant rank module over semilocal ring is free (#31241) …
Added Module.free_of_flat_of_finrank_eqView on Github →