Theorem TensorProduct.Algebra.exists_of_fg

Modification history

2025-09-19 07:04
Mathlib/RingTheory/TensorProduct/DirectLimitFG.lean
chore(*): drop some `Decidable`/`Fintype` assumptions (#29785) …
Modified TensorProduct.Algebra.exists_of_fgView on Github →
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 TensorProduct.Algebra.exists_of_fgView on Github →