zero_notMem_nonZeroDivisorsLeft

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

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

English

0 is not a left non-zero divisor: 0 ∉ nonZeroDivisorsLeft M0.

Русский

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

LaTeX

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

Lean4

theorem zero_notMem_nonZeroDivisorsLeft : 0 ∉ nonZeroDivisorsLeft M₀ := fun h ↦ one_ne_zero <| h 1 <| zero_mul _

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

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

Разделы

Аффилиация

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