The star structure on tensor products

This file defines the Star structure on tensor products. This also defines the StarAddMonoid and StarModule instances for tensor products.

instance TensorProduct.instStar {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : Star (TensorProduct R A B)

@[simp]

theorem TensorProduct.star_tmul {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] (x : A) (y : B) : star (x ⊗ₜ[R] y) = star x ⊗ₜ[R] star y

noncomputable instance TensorProduct.instInvolutiveStar {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : InvolutiveStar (TensorProduct R A B)

noncomputable instance TensorProduct.instStarAddMonoid {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : StarAddMonoid (TensorProduct R A B)

instance TensorProduct.instStarModule {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : StarModule R (TensorProduct R A B)

theorem starLinearEquiv_tensor {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [AddCommMonoid B] [StarAddMonoid B] [Module R B] [StarModule R B] : starLinearEquiv R = TensorProduct.congr (starLinearEquiv R) (starLinearEquiv R)