instIsTorsionFree

Mathlib.Algebra.Module.Torsion

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

English

As above, existence of a common nonzero tester across duals in a finite family.

Русский

Как выше, существование общего ненулевого тестера для двойственных отображений в конечной семье.

LaTeX

$$$$ \\exists x, \\forall i, f_i x \\neq 0. $$$$

Lean4

instance : IsTorsionFree R R where isSMulRegular _r hr := hr.1

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

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

Разделы

Аффилиация

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