instDiv

Mathlib.Algebra.Notation.Prod

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

English

The product with division is coordinatewise: (g,h) / (g',h') = (g/g', h/h').

Русский

Деление в произведении задаётся координатно: (g,h) / (g',h') = (g/g', h/h').

LaTeX

$$ (g,h) / (g',h') = (g/g', h/h') $$

Lean4

@[to_additive]
instance instDiv : Div (G × H) :=
  ⟨fun p q => ⟨p.1 / q.1, p.2 / q.2⟩⟩

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

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

Разделы

Аффилиация

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