instPow

Mathlib.Topology.LocallyConstant.Algebra

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

English

If Y has a power operation, LocallyConstant X Y inherits a power operation defined pointwise: (f^n)(x) = f(x)^n.

Русский

Если у Y есть операция возведения в степень, LocallyConstant X Y получает аналогичную по точкам: (f^n)(x) = f(x)^n.

LaTeX

$$$(f^n)(x) = f(x)^n.$$$

Lean4

@[to_additive existing LocallyConstant.smul]
instance [Pow Y α] : Pow (LocallyConstant X Y) α where pow f n := f.map (· ^ n)

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

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

Разделы

Аффилиация

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