div_def — Mathlib

English

Division in the DirectLimit corresponds to division at representatives: [i,x] / [i,y] equals [i, x/y].

Русский

Деление в прямом пределе соответствует делению на представителях: [i,x] / [i,y] = [i, x/y].

LaTeX

$$$\\frac{\\langle i,x\\rangle}{\\langle i,y\\rangle} = \\langle i, \\frac{x}{y}\\rangle$ in DirectLimit$$

Lean4

@[to_additive]
theorem div_def (i x y) : ⟦⟨i, x⟩⟧ / ⟦⟨i, y⟩⟧ = (⟦⟨i, x / y⟩⟧ : DirectLimit G f) :=
  map₂_def ..

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