Commit 2025-07-30 17:41 e03d39f0

View on Github →

fix(LinearAlgebra/TensorProduct): fix ⊗[R] precedence (#27590) This PR makes ⊗[R] have the same precedence as the infixl ⊗ notation. And it fixes the brackets where necessary.

Estimated changes

Modified Mathlib/Algebra/Category/CoalgCat/ComonEquivalence.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Associator.lean

modified def TensorProduct.leftComm

modified theorem TensorProduct.map_map_assoc

modified def TensorProduct.rightComm

modified def TensorProduct.tensorTensorTensorAssoc

modified def TensorProduct.tensorTensorTensorComm

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

modified theorem TensorProduct.ext_fourfold'

modified theorem TensorProduct.ext_fourfold

modified theorem TensorProduct.ext_threefold

Modified Mathlib/RingTheory/Coalgebra/TensorProduct.lean

Modified Mathlib/RingTheory/IsTensorProduct.lean

Modified Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean

Modified Mathlib/RingTheory/TensorProduct/Basic.lean

modified def Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct

modified def Algebra.TensorProduct.leftComm

modified def Algebra.TensorProduct.tensorTensorTensorComm