init_pow — Mathlib

English

Init distributes over exponentiation: init(n)(x^m) = init(n)(init(n)(x)^m).

Русский

Init распределяется по возведению в степень: init(n)(x^m) = init(n)(init(n)(x)^m).

LaTeX

$$$$\operatorname{init}_n(x^m) = \operatorname{init}_n(\operatorname{init}_n x)^m.$$$$

Lean4

theorem init_pow (m : ℕ) (x : 𝕎 R) (n : ℕ) : init n (x ^ m) = init n (init n x ^ m) := by
  init_ring using fun p [Fact (Nat.Prime p)] n => wittPow_vars p m n

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