theorem IsSimpleRing.left_of_tensor (K : Type u) [Field K] (B C : Type u) [Ring B] [Ring C] [Algebra K C] [Algebra K B] [hbc : IsSimpleRing (TensorProduct K B C)] : IsSimpleRing B

theorem IsSimpleRing.right_of_tensor (K : Type u) [Field K] (B C : Type u) [Ring B] [Ring C] [Algebra K C] [Algebra K B] [hbc : IsSimpleRing (TensorProduct K B C)] : IsSimpleRing C