Theorem starLinearEquiv_tensor

Modification history

2025-10-31 17:31

Mathlib/Algebra/Star/TensorProduct.lean

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

Added starLinearEquiv_tensor View on Github →