Def PiTensorProduct.liftAlgHom

Modification history

2026-10-29 21:19

Mathlib/RingTheory/PiTensorProduct.lean

feat(LinearAlgebra/MultilinearMap): notation for `MultilinearMap` (#43877) …

Modified PiTensorProduct.liftAlgHom View on Github →

2024-03-02 20:50

Mathlib/RingTheory/PiTensorProduct.lean

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

Added PiTensorProduct.liftAlgHom View on Github →