Commit 2023-09-29 14:27 3d729341

feat(RingTheory/TensorProduct): the universal property of the tensor product of algebras (#7409) The construction used for CliffordAlgebra.ofBaseChange generalizes into a universal property for building arbitrary algebra morphisms out of the tensor product. It turns out this is a known result; it is mentioned at https://en.wikipedia.org/wiki/Tensor_product_of_algebras#Further_properties which cites the linked reference, though the version added by this PR is heterobasic like the rest of this file. This is a generalization of the existing Algebra.TensorProduct.productLeftAlgHom to non-commutative rings.