Lemmas about tensor products

theorem TensorProduct.prodRight_fst {R : Type u_1} {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [Invertible 2] [Invertible 2] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (x : TensorProduct R A (M₁ × M₂)) : ((prodRight R A A M₁ M₂) x).1 = (LinearMap.baseChange A (LinearMap.fst R M₁ M₂)) x

theorem TensorProduct.prodRight_snd {R : Type u_1} {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [Invertible 2] [Invertible 2] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] (x : TensorProduct R A (M₁ × M₂)) : ((prodRight R A A M₁ M₂) x).2 = (LinearMap.baseChange A (LinearMap.snd R M₁ M₂)) x