instCommMagmaOfInvertibleOfNat

Mathlib.Algebra.Symmetrized

URI: https://scilib.ai/kg/mathlib#SymAlg.instCommMagmaOfInvertibleOfNat

English

If α is a ring and 2 is invertible, then α^{sym} is a commutative magma.

Русский

Если α — кольцо и 2 обратимо, то α^{sym} является коммутативной магмой.

LaTeX

$$CommMagma(α^{sym})$$

Lean4

instance [Ring α] [Invertible (2 : α)] : CommMagma αˢʸᵐ where mul_comm := SymAlg.mul_comm

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

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

Разделы

Аффилиация

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