mul_mem_nonunits_right

Mathlib.RingTheory.Ideal.Nonunits

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

English

If b is a nonunit in a commutative monoid, then a*b is also a nonunit for any a.

Русский

Если b не единица в коммутативном моноиде, то и a·b не единица для любого a.

LaTeX

$$b \in nonunits(\alpha) \Rightarrow a * b \in nonunits(\alpha)$$

Lean4

theorem mul_mem_nonunits_right [CommMonoid α] : b ∈ nonunits α → a * b ∈ nonunits α :=
  mt isUnit_of_mul_isUnit_right

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

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

Разделы

Аффилиация

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