coe_smul

Mathlib.Algebra.Star.NonUnitalSubalgebra

URI: https://scilib.ai/kg/mathlib#NonUnitalStarSubalgebra.coe_smul

English

There exists an SMulCommClass for the subtype S with R A A

Русский

Существует SMulCommClass для подтипа S с R A A

LaTeX

$$instSMulCommClass$$

Lean4

@[simp, norm_cast]
theorem coe_smul [SMul R' R] [SMul R' A] [IsScalarTower R' R A] (r : R') (x : S) : ↑(r • x) = r • (x : A) :=
  rfl

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

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

Разделы

Аффилиация

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