prodComm

Mathlib.Algebra.Ring.Prod

URI: https://scilib.ai/kg/mathlib#RingEquiv.prodComm

English

Swapping coordinates induces a ring equivalence between the product rings: R × S ≃+* S × R.

Русский

Перестановка координат задаёт эквивалентность колец: R × S ≃+* S × R.

LaTeX

$$$ \\text{prodComm} : R \\times S \\simeq+* S \\times R. $$$

Lean4

/-- Swapping components as an equivalence of (semi)rings. -/
def prodComm : R × S ≃+* S × R :=
  { AddEquiv.prodComm, MulEquiv.prodComm with }

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

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

Разделы

Аффилиация

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