ofMul_mul

Mathlib.Algebra.Group.TypeTags.Basic

URI: https://scilib.ai/kg/mathlib#ofMul_mul

English

The toMul map sends the additive structure on α into the multiplicative structure: (x + y).toMul = x.toMul * y.toMul.

Русский

Переход кMul переводит аддитивную структуру на α в умножительную: (x + y).toMul = x.toMul * y.toMul.

LaTeX

$$toMul_add [Mul α] (x y : Additive α) : (x + y).toMul = x.toMul * y.toMul$$

Lean4

@[simp]
theorem ofMul_mul [Mul α] (x y : α) : ofMul (x * y) = ofMul x + ofMul y :=
  rfl

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

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

Разделы

Аффилиация

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