zpow₀_def — Mathlib

English

In a directed system with a division operation and a monoid with zero, the quotient in DirectLimit satisfies the natural compatibility: the quotient of ⟦⟨i,x⟩⟧ by ⟦⟨i,y⟩⟧ equals ⟦⟨i, x/y⟩⟧.

Русский

В направленном пределе с операцией деления и нулевым элементом выполнено совместимостное тождество: деление классов ⟦⟨i,x⟩⟧ на ⟦⟨i,y⟩⟧ равно классу ⟦⟨i, x/y⟩⟧.

LaTeX

$$$\overline{\langle i,x \rangle} / \overline{\langle i,y \rangle} = \overline{\langle i, x/y \rangle}$$$

Lean4

theorem zpow₀_def (i x) (n : ℤ) : ⟦⟨i, x⟩⟧ ^ n = (⟦⟨i, x ^ n⟩⟧ : DirectLimit G f) :=
  rfl

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