ofRat_inv — Mathlib

English

The image of x⁻¹ equals the inverse of the image of x in CauSeq.Completion.Cauchy abv.

Русский

Образ x⁻¹ равен обратному образу x в CauSeq.Completion.Cauchy abv.

LaTeX

$$$\operatorname{ofRat}(x^{-1}) = (\operatorname{ofRat}x)^{-1}$$$

Lean4

theorem ofRat_inv (x : β) : ofRat x⁻¹ = ((ofRat x)⁻¹ : (Cauchy abv)) :=
  congr_arg mk <| by split_ifs with h <;> [simp only [const_limZero.1 h, GroupWithZero.inv_zero, const_zero]; rfl]

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