instPow

Mathlib.Algebra.Notation.Prod

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

English

There is a coordinatewise power on the product: (p)^c = (p1^c, p2^c).

Русский

На произведении существует координатная возводимость: (p)^c = (p1^c, p2^c).

LaTeX

$$(p^c) = (p_1^c, p_2^c)$$

Lean4

@[to_additive existing instSMul]
instance instPow : Pow (α × β) E where pow p c := (p.1 ^ c, p.2 ^ c)

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

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

Разделы

Аффилиация

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