Commit 2025-10-31 17:31 2cabfc5d

View on Github →

feat(Algebra/Star/LinearMap): star mul' = mul' ∘ TensorProduct.comm and star (f ⊗ₘ g) = star f ⊗ₘ star g (#31003)

Estimated changes

Modified Mathlib/Algebra/Star/LinearMap.lean

added theorem LinearMap.intrinsicStar_lTensor

added theorem LinearMap.intrinsicStar_mul'

added theorem LinearMap.intrinsicStar_rTensor

added theorem TensorProduct.intrinsicStar_map

Modified Mathlib/Algebra/Star/TensorProduct.lean

added theorem starLinearEquiv_tensor

Modified Mathlib/LinearAlgebra/TensorProduct/Basic.lean

added theorem TensorProduct.congr_congr

modified theorem TensorProduct.congr_trans