Theorem Submodule.exists_fg_le_eq_rTensor_inclusion

Modification history

2024-11-14 10:43
Mathlib/RingTheory/Finiteness.lean
chore(RingTheory): split Finiteness.lean into many smaller files (#18964) …
Modified Submodule.exists_fg_le_eq_rTensor_inclusionView on Github →
2023-11-19 22:31
Mathlib/RingTheory/Finiteness.lean
Extend RingTheory.Flat.iff_rTensor_injective to all ideals (#8494) …
Added Submodule.exists_fg_le_eq_rTensor_inclusionView on Github →