mathlib3

41ced1ca - feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900)

feat(ring_theory/tensor_product): The tensor product `A ⊗ B` is generated by tensors `a ⊗ₜ b` (#10900) The tensor product is generated by tensors, in terms of `algebra.adjoin`. This is an immediate consequence of `span_tmul_eq_top`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>