isSMulRegular

Mathlib.Algebra.Regular.SMul

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

English

If a is left-regular in a multiplicative structure, then a is SMul-regular for any SMul action.

Русский

Если элемент лево-регулярен в мультипликативной структуре, то он является SMul-регулярным для любого действия SMul.

LaTeX

$$IsLeftRegular a \Rightarrow IsSMulRegular R a$$

Lean4

theorem isSMulRegular [Mul R] {c : R} (h : IsLeftRegular c) : IsSMulRegular R c :=
  h

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

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

Разделы

Аффилиация

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