coe_pow

Mathlib.Order.Filter.Germ.Basic

URI: https://scilib.ai/kg/mathlib#Filter.Germ.coe_pow

English

The germ of a power and the power of a germ agree: (f^n) lifted to germs equals the germ of f lifted to the nth power.

Русский

Жермa степени согласуется со степенью жерма: $\\uparrow(f^n) = (\\uparrow f)^n$.

LaTeX

$$$[Pow\\ G\\ M] (f,n) : \\uparrow(f^n) = (\\uparrow f)^n.$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem coe_pow [Pow G M] (f : α → G) (n : M) : ↑(f ^ n) = (f : Germ l G) ^ n :=
  rfl

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

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

Разделы

Аффилиация

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