zpow_def — Mathlib

English

Same as above for zero-inclusive/division with zero-handling: the division in DirectLimit is given by representatives.

Русский

То же самое для деления с учётом нуля: деление в прямом пределе задаётся через представителя.

LaTeX

$$$\\mathrm{div}_{DirectLimit}$ is given by $[i,x]/[i,y] = [i, x/y]$$$

Lean4

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

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