zero_notMem_nonZeroDivisors

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

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

English

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

Русский

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

LaTeX

$$$ 0 \notin M_0^{0}$$$

Lean4

theorem zero_notMem_nonZeroDivisors : 0 ∉ M₀⁰ := fun h ↦ zero_notMem_nonZeroDivisorsLeft h.1

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

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

Разделы

Аффилиация

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