Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-16 11:29 624716b7

View on Github →

feat(ring_theory/tensor_product): A-algebra structure on A' ⊗[R] B. (#15241)

Estimated changes

Modified src/ring_theory/tensor_product.lean

modified theorem algebra.tensor_product.algebra_map_apply

added def algebra.tensor_product.include_left_ring_hom

added def algebra.tensor_product.product_left_alg_hom

modified theorem algebra.tensor_product.product_map_left_apply

deleted def algebra.tensor_product.tensor_algebra_map