one_mk_mul_one_mk

Mathlib.Algebra.Group.Prod

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

English

In the product of two structures M × N, (1, b1) · (1, b2) = (1, b1 b2).

Русский

В произведении структур M × N произведение (1, b1) и (1, b2) даёт (1, b1 b2).

LaTeX

$$$((1 : M), b_1) \cdot (1, b_2) = (1, b_1 \cdot b_2)$$$

Lean4

@[to_additive]
theorem one_mk_mul_one_mk [MulOneClass M] [Mul N] (b₁ b₂ : N) : ((1 : M), b₁) * (1, b₂) = (1, b₁ * b₂) := by
  rw [mk_mul_mk, mul_one]

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

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

Разделы

Аффилиация

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