LeanPool.BrauerGroupNew.LemmasAboutSimpleRing #
Imported Lean Pool material for LeanPool.BrauerGroupNew.LemmasAboutSimpleRing.
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)]
:
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)]
: