Theorem Submodule.FG.exists_rTensor_fg_inclusion_eq

Modification history

2025-01-02 19:57
Mathlib/Algebra/Colimit/TensorProduct.lean
feat(Algebra/Colimit): the directed system of finitely generated submodules (#20264) …
Added Submodule.FG.exists_rTensor_fg_inclusion_eqView on Github →