Def PiTensorProduct.piTensorHomMap

Modification history

2024-03-02 20:50

Mathlib/LinearAlgebra/PiTensorProduct.lean

feat(LinearAlgebra/PiTensorProduct): arbitrary tensor product of algebras (#9395) …

Added PiTensorProduct.piTensorHomMap View on Github →