npow_def — Mathlib

English

Powers in the direct limit correspond to powers of representatives: ⟦⟨i,x⟩⟧^n = ⟦⟨i,x^n⟩⟧.

Русский

Степени в предельном лимите соответствуют степеням представителей: ⟦⟨i,x⟩⟧^n = ⟦⟨i,x^n⟩⟧.

LaTeX

$$$ \forall i,x,n:\; \llbracket i, x \rrbracket ^ n = \llbracket i, x^n \rrbracket $$$

Lean4

@[to_additive]
theorem npow_def (i x) (n : ℕ) : ⟦⟨i, x⟩⟧ ^ n = (⟦⟨i, x ^ n⟩⟧ : DirectLimit G f) :=
  rfl

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