Theorem Submodule.exists_fg_le_eq_rTensor_inclusion

Modification history

2025-01-02 11:03
Mathlib/RingTheory/Finiteness/TensorProduct.lean
feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)
Modified Submodule.exists_fg_le_eq_rTensor_inclusionView on Github →
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 →