[Merged by Bors] - chore(RingTheory/TensorProduct/Basic): some API for includeLeft and includeRight#39694

themathqueen wants to merge 4 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

themathqueen:tensorProduct_apithemathqueen/mathlib4:tensorProduct_apiCopy head branch name to clipboard