[Merged by Bors] - feat(LinearAlgebra/PiTensorProduct): arbitrary tensor product of algebras#9395

jjaassoonn wants to merge 71 commits into

masterleanprover-community/mathlib4:masterfrom

zjj/tensorProductAlgebraleanprover-community/mathlib4:zjj/tensorProductAlgebraCopy head branch name to clipboard