English
If G has a Pow structure with M (Pow G M), then Germ_l G has a Pow structure, defined by (f)^n := map (·^n) f; in particular, the germ-power corresponds to the germ of the pointwise power.
Русский
Если у G есть структура возведения в степень с M (Pow G M), то Germ_l G также имеет структуру возведения в степень, определяемую (f)^n := map (·^n) f; следовательно, возведение в степень сохраняется через жермы.
LaTeX
$$$[Pow\\ G\\ M] \\Rightarrow Pow(\\mathrm{Germ}_l G)\\ M,$ с определением $f^n := \\mathrm{map}(\\cdot^n)\\ f$; и для любого f, n: $\\uparrow(f^n) = (\\uparrow f)^n$.$$
Lean4
@[to_additive existing instSMul]
instance instPow [Pow G M] : Pow (Germ l G) M where pow f n := map (· ^ n) f
