of_mul

Mathlib.Algebra.Regular.SMul

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

← MathLib Explorer

English

If IsSMulRegular M (a*b) holds, then IsSMulRegular M b holds.

Русский

Если IsSMulRegular M (a*b) выполнено, тогда IsSMulRegular M b выполняется.

LaTeX

$$IsSMulRegular M (instHMul.hMul a b) → IsSMulRegular M b$$

Lean4

theorem of_mul [Mul R] [IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) : IsSMulRegular M b :=
  by
  rw [← smul_eq_mul] at ab
  exact ab.of_smul _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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