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

Commit

3 years ago

feat(ring_theory/tensor_product): `A`-algebra structure on `A' ⊗[R] B`. (#15241) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>

Author

erdOne

Parents

316d1886

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

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