mul

Mathlib.Algebra.Regular.SMul

URI: https://scilib.ai/kg/mathlib#IsSMulRegular.mul

English

If a and b are SMul-regular, then a * b is SMul-regular.

Русский

Если a и b — SMul-регулярны, то a * b — SMul-регулярно.

LaTeX

$$IsSMulRegular M a → IsSMulRegular M b → IsSMulRegular M (a * b)$$

Lean4

theorem mul [Mul R] [IsScalarTower R R M] (ra : IsSMulRegular M a) (rb : IsSMulRegular M b) : IsSMulRegular M (a * b) :=
  ra.smul rb

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

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

Разделы

Аффилиация

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