mul_mem_nonunits_left

Mathlib.RingTheory.Ideal.Nonunits

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mul_mem_nonunits_left [CommMonoid α] : a ∈ nonunits α → a * b ∈ nonunits α :=
  mt isUnit_of_mul_isUnit_left

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

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

Разделы

Аффилиация

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