instNoZeroDivisors

Mathlib.Algebra.GroupWithZero.Associated

URI: https://scilib.ai/kg/mathlib#Associates.instNoZeroDivisors

English

Associates M has no zero divisors when M has CancelMonoidWithZero structure.

Русский

У Associates(M) нет нулевых делителей при наличии структуры CancelMonoidWithZero на M.

LaTeX

$$$ \operatorname{NoZeroDivisors}(\mathrm{Associates}(M)) $$$

Lean4

instance : NoZeroDivisors (Associates M) := by infer_instance

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

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

Разделы

Аффилиация

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