Theorem Submodule.exists_fg_of_baseChange_eq_zero

Modification history

2025-07-16 13:02
Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean
feat(RingTheory/TensorProduct/FG) : direct limit properties of tensor products wrt finitely generated submodules (#26717) …
Added Submodule.exists_fg_of_baseChange_eq_zeroView on Github →