init_init — Mathlib

English

Applying the initialization operation twice with the same n yields the same result as applying it once: init(n, init(n, x)) = init(n, x).

Русский

Применение операции инициализации дважды подряд с тем же n даёт тот же результат, что и одно применение: init(n, init(n, x)) = init(n, x).

LaTeX

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

Lean4

@[simp]
theorem init_init (x : 𝕎 R) (n : ℕ) : init n (init n x) = init n x := by init_ring

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