div_def

Mathlib.Algebra.Notation.Prod

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

English

The product quotient is coordinatewise: a / b = (a1 / b1, a2 / b2).

Русский

Частное от пары задано координатно: a / b = (a1 / b1, a2 / b2).

LaTeX

$$a / b = (a_1 / b_1, a_2 / b_2)$$

Lean4

@[to_additive]
theorem div_def (a b : G × H) : a / b = (a.1 / b.1, a.2 / b.2) :=
  rfl

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

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

Разделы

Аффилиация

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