mul_right

Mathlib.Algebra.Ring.Invertible

URI: https://scilib.ai/kg/mathlib#IsAddUnit.mul_right

English

If x is an additive unit, then for any y, x * y is an additive unit.

Русский

Если x — добавочная единица, то для любого y верно, что x * y — добавочная единица.

LaTeX

$$IsAddUnit x \rightarrow \forall y, IsAddUnit (x * y)$$

Lean4

theorem mul_right {x : R} (h : IsAddUnit x) (y : R) : IsAddUnit (x * y) :=
  (h.addUnit.mulRight y).isAddUnit

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

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

Разделы

Аффилиация

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