Commit 2023-07-27 13:17 00269a6f

View on Github →

chore(linear_algebra/tensor_product): forward-port leanprover-community/mathlib#19143 (#6094)

Estimated changes

Modified Mathlib/CategoryTheory/Monoidal/Internal/Module.lean

Modified Mathlib/LinearAlgebra/TensorProduct.lean

Modified Mathlib/RingTheory/Kaehler.lean

Modified Mathlib/RingTheory/TensorProduct.lean

deleted theorem Algebra.TensorProduct.mul_one

deleted theorem Algebra.TensorProduct.one_mul