ofCauchy_div — Mathlib

English

Division in the Cauchy completion respects the quotient of representatives: the image of f/g equals the image of f divided by the image of g.

Русский

Деление в завершении по Коши сохраняет деление на представителей: образ f/g равен образу f делённому на образ g.

LaTeX

$$$\langle f/g\rangle = \langle f\rangle/\langle g\rangle$$$

Lean4

theorem ofCauchy_div (f g) : (⟨f / g⟩ : ℝ) = (⟨f⟩ : ℝ) / (⟨g⟩ : ℝ) := by
  simp_rw [div_eq_mul_inv, ofCauchy_mul, ofCauchy_inv]

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