instOne

Mathlib.Algebra.Notation.Prod

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

English

There is a canonical unit on the product M × N given by (1,1).

Русский

Существует каноническая единица на произведении M × N: (1,1).

LaTeX

$$$1_{M\times N} = (1_M, 1_N)$$$

Lean4

@[to_additive]
instance instOne : One (M × N) :=
  ⟨(1, 1)⟩

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

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

Разделы

Аффилиация

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