noZeroSMulDivisors

Mathlib.Algebra.Module.Torsion

URI: https://scilib.ai/kg/mathlib#Submodule.QuotientTorsion.noZeroSMulDivisors

English

NoZeroSMulDivisors holds for quotient by torsion torsion.

Русский

NoZeroSMulDivisors сохраняется в фактормодуле по торсии.

LaTeX

$$QuotientTorsion.noZeroSMulDivisors$$

Lean4

instance noZeroSMulDivisors [IsDomain R] : NoZeroSMulDivisors R (M ⧸ torsion R M) :=
  noZeroSMulDivisors_iff_torsion_eq_bot.mpr torsion_eq_bot

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

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

Разделы

Аффилиация

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