Mathlib Changelog
v4
Changelog
About
Github
Theorem
Algebra.TensorProduct.mk_one_injective_of_isScalarTower
Modification history
2025-04-11 17:23
Mathlib/RingTheory/TensorProduct/Basic.lean
feat: generalize rest of Mathlib.RingTheory (#23194) …
Modified
Algebra.TensorProduct.mk_one_injective_of_isScalarTower
View on Github →
2025-02-12 21:23
Mathlib/RingTheory/TensorProduct/Basic.lean
feat(RingTheory/FaithfullyFlat): equivalent characterizations for algebras (#20725) …
Added
Algebra.TensorProduct.mk_one_injective_of_isScalarTower
View on Github →