Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-09-27 03:37
ad44c68b
View on Github →
chore(RingTheory/TensorProduct): extra lemmas about
{nat,int}Cast
(
#7391
)
Estimated changes
Modified
Mathlib/RingTheory/TensorProduct.lean
added
theorem
Algebra.TensorProduct.intCast_def'
added
theorem
Algebra.TensorProduct.natCast_def'