isSMulRegular

Mathlib.Algebra.Regular.SMul

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

English

If a is right-regular, then MulOpposite.op a is SMul-regular.

Русский

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

LaTeX

$$IsRightRegular a \Rightarrow IsSMulRegular R (MulOpposite.op a)$$

Lean4

theorem isSMulRegular [Mul R] {c : R} (h : IsRightRegular c) : IsSMulRegular R (MulOpposite.op c) :=
  h

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

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

Разделы

Аффилиация

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