Commit 2025-08-20 00:04 f0549db4

View on Github →

chore(TensorProduct): group structure from the first factor only (#28660) Needed to show AddLocalization (⊤ : AddSubmonoid M) ≃+ ℤ ⊗[ℕ] M.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

modified theorem LinearMap.rTensor_neg

modified theorem LinearMap.rTensor_sub

modified theorem TensorProduct.tmul_neg

modified theorem TensorProduct.tmul_sub

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified theorem Algebra.TensorProduct.intCast_def'