toOpposite

Mathlib.Algebra.Algebra.Opposite

URI: https://scilib.ai/kg/mathlib#AlgEquiv.toOpposite

← MathLib Explorer

English

A commutative algebra A is isomorphic to its opposite A^op as an R-algebra.

Русский

Коммутативная алгебра A изоморфна своей противоположности A^{op} как R-алгебра.

LaTeX

$$$ A^{op} \\cong_R A $$$

Lean4

/-- A commutative algebra is isomorphic to its opposite. -/
@[simps!]
def toOpposite : A ≃ₐ[R] Aᵐᵒᵖ where
  __ := RingEquiv.toOpposite A
  commutes' _r := rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru