mk_mul_mk

Mathlib.Algebra.Notation.Prod

URI: https://scilib.ai/kg/mathlib#Prod.mk_mul_mk

English

Under coordinatewise multiplication, the product of pairs is (a1, b1) · (a2, b2) = (a1 a2, b1 b2).

Русский

При координатном перемножении пар произведение равно (a1, b1) · (a2, b2) = (a1 a2, b1 b2).

LaTeX

$$$(a_1,b_1) \cdot (a_2,b_2) = (a_1 a_2, b_1 b_2)$$$

Lean4

@[to_additive (attr := simp)]
theorem mk_mul_mk (a₁ a₂ : M) (b₁ b₂ : N) : (a₁, b₁) * (a₂, b₂) = (a₁ * a₂, b₁ * b₂) :=
  rfl

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

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

Разделы

Аффилиация

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