mem_nonZeroDivisorsLeft

Mathlib.Algebra.GroupWithZero.NonZeroDivisors

URI: https://scilib.ai/kg/mathlib#IsLeftRegular.mem_nonZeroDivisorsLeft

English

If r is left regular, then r ∈ nonZeroDivisorsLeft.

Русский

Если r слева регулярный, то r ∈ не нулевые делители слева.

LaTeX

$$$ (h : IsLeftRegular r) \Rightarrow r \in \operatorname{nonZeroDivisorsLeft}(M_0)$$$

Lean4

theorem mem_nonZeroDivisorsLeft (h : IsLeftRegular r) : r ∈ nonZeroDivisorsLeft M₀ := fun _x hx ↦
  h.mul_left_eq_zero_iff.mp hx

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

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

Разделы

Аффилиация

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