isTorsionBySet_cotangent

Mathlib.RingTheory.Ideal.Cotangent

URI: https://scilib.ai/kg/mathlib#Ideal.isTorsionBySet_cotangent

English

I.Cotangent is torsion by the set I: module IsTorsionBySet R I.Cotangent I holds.

Русский

I.Cotangent является торионным по множеству I.

LaTeX

$$$\\text{Module.IsTorsionBySet } R I.Cotangent I$$$

Lean4

theorem isTorsionBySet_cotangent : Module.IsTorsionBySet R I.Cotangent I := fun m x ↦ m.smul_eq_zero_of_mem x.2

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

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

Разделы

Аффилиация

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