English
Let {A_i} be a family of R-algebras indexed by i. Then the opposite algebra of the direct product is isomorphic to the direct product of the opposite algebras: (∏_i A_i)ᵒᵖ ≅ₐ[R] ∏_i (A_i)ᵒᵖ.
Русский
Пусть {A_i} — семейство R-алгебр, индексируемое i. Тогда противоположная алгебра прямого произведения изоморфна прямому произведению противоположных алгебр: (∏_i A_i)^{op} ≅ₐ[R] ∏_i (A_i)^{op}.
LaTeX
$$$$(\prod_i A_i)^{\mathrm{op}} \cong_R \prod_i (A_i^{\mathrm{op}}).$$$$
Lean4
/-- The opposite of a direct product is isomorphic to the direct product of the opposites as
algebras. -/
def piMulOpposite : (Π i, A₁ i)ᵐᵒᵖ ≃ₐ[R] Π i, (A₁ i)ᵐᵒᵖ
where
__ := RingEquiv.piMulOpposite A₁
commutes' _ := rfl
