Mathlib Changelog
v4
Changelog
About
Github
Theorem
TensorProduct.toLinearMap_congr
Modification history
2025-07-25 10:25
Mathlib/LinearAlgebra/TensorProduct/Basic.lean
feat(LinearAlgebra/TensorProduct): `map f₂ g₂ (map f₁ g₁ x) = map (f₂ ∘ₗ f₁) (g₂ ∘ₗ g₁) x` (#27142) …
Added
TensorProduct.toLinearMap_congr
View on Github →