instIsTorsionFreeMulOpposite

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Module.instIsTorsionFreeMulOpposite

English

The ring R is torsion-free as a left module over its opposite ring R^op.

Русский

Кольцо R тожностно свободно как модуль над левым кольцом R^op.

LaTeX

$$$$ \\text{IsTorsionFree}_{R^{\\mathrm{op}}} (R). $$$$

Lean4

instance : IsTorsionFree Rᵐᵒᵖ R where isSMulRegular _r hr := hr.unop.2

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

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

Разделы

Аффилиация

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