mk_one_mul_mk_one

Mathlib.Algebra.Group.Prod

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

English

In M × N, (a1, 1) · (a2, 1) = (a1 a2, 1).

Русский

В произведении M × N, (a1, 1) · (a2, 1) = (a1 a2, 1).

LaTeX

$$$ (a_1, 1) \cdot (a_2, 1) = (a_1 a_2, 1) $$$

Lean4

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

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

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

Разделы

Аффилиация

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