mul_left

Mathlib.Algebra.Ring.Invertible

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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