zero_notMem_nonZeroDivisorsRight

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#zero_notMem_nonZeroDivisorsRight

English

0 is not a right non-zero divisor: 0 ∉ nonZeroDivisorsRight M0.

Русский

0 не является правым не нулевым делителем: 0 ∉ nonZeroDivisorsRight M0.

LaTeX

$$$ 0 \notin \operatorname{nonZeroDivisorsRight}(M_0)$$$

Lean4

theorem zero_notMem_nonZeroDivisorsRight : 0 ∉ nonZeroDivisorsRight M₀ := fun h ↦ one_ne_zero <| h 1 <| mul_zero _

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

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

Разделы

Аффилиация

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