toMul_add

Mathlib.Algebra.Group.TypeTags.Basic

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

English

The isomorphism toMul preserves multiplication structure from Additive α to α, i.e., (x*y).toMul = x.toMul * y.toMul.

Русский

Изоморфизм toMul сохраняет структуру умножения: (x*y).toMul = x.toMul * y.toMul.

LaTeX

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

Lean4

@[simp]
theorem toMul_add [Mul α] (x y : Additive α) : (x + y).toMul = x.toMul * y.toMul :=
  rfl

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

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

Разделы

Аффилиация

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