Theorem Submodule.exists_fg_le_subset_range_rTensor_inclusion

Modification history

2025-03-05 15:27

Mathlib/RingTheory/Finiteness/TensorProduct.lean

chore(RingTheory): merge `Finiteness/TensorProduct.lean` into `TensorProduct/Finite.lean` (#22595) …

Modified Submodule.exists_fg_le_subset_range_rTensor_inclusion View on Github →

2025-01-02 11:03

Mathlib/RingTheory/Finiteness/TensorProduct.lean

feat(Algebra): auxiliary lemmas for flatness over semirings (#20265)

Added Submodule.exists_fg_le_subset_range_rTensor_inclusion View on Github →