instSMulCommClass

Mathlib.Algebra.Algebra.Rat

URI: https://scilib.ai/kg/mathlib#Rat.instSMulCommClass

English

If you have SMulCommClass R S S and Rat, then Rat inherits SMulCommClass with R, i.e., Rat SMulCommClass R S.

Русский

Если существует SMulCommClass R S S, то Rat наследует SMulCommClass R S.

LaTeX

$$$$ \\text{SMulCommClass } R S S $$$$

Lean4

instance instSMulCommClass [SMulCommClass R S S] : SMulCommClass ℚ R S where
  smul_comm q a b := by simp [smul_def, mul_smul_comm]

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

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

Разделы

Аффилиация

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