instPowCauchyNat

Mathlib.Algebra.Order.CauSeq.Completion

URI: https://scilib.ai/kg/mathlib#CauSeq.Completion.instPowCauchyNat

English

The natural-power operation on the completion is induced by taking powers of sequences: mk f raised to n equals mk (f^n).

Русский

Возведение в натуральную степень на завершении определяется покомпонентно: mk f^n = mk (f^n).

LaTeX

$$$(\mathrm{mk} f)^n = \mathrm{mk}(f^n)$$$

Lean4

instance : Pow (Cauchy abv) ℕ :=
  ⟨fun x n => Quotient.map (· ^ n) (fun _ _ hf => pow_equiv_pow hf _) x⟩

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

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

Разделы

Аффилиация

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