inl_mul_inr_eq_mk

Mathlib.Algebra.Order.Monoid.Lex

URI: https://scilib.ai/kg/mathlib#OrderMonoidHom.inl_mul_inr_eq_mk

English

The product of the images inl m and inr n equals the pair (m, n): inl(m) · inr(n) = (m, n).

Русский

Произведение образов inl m и inr n равно паре (m, n): inl(m) · inr(n) = (m, n).

LaTeX

$$$$ inl_{\alpha,\beta}(m) \cdot inr_{\alpha,\beta}(n) = (m,n). $$$$

Lean4

@[to_additive]
theorem inl_mul_inr_eq_mk (m : α) (n : β) : inl α β m * inr α β n = (m, n) := by simp

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

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

Разделы

Аффилиация

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