associated_num_den_inv — Mathlib

English

If x ≠ 0, the numerator of x and the denominator of x^{-1} are associated.

Русский

Если x ≠ 0, числитель x и знаменатель x^{-1} являются ассоциированными.

LaTeX

$$$\\mathrm{Associated}(\\mathrm{num}_A(x), \\mathrm{den}_A(x^{-1}))$$$

Lean4

theorem associated_num_den_inv (x : K) (hx : x ≠ 0) : Associated (num A x : A) (den A x⁻¹) :=
  by
  have : Associated (num A x⁻¹⁻¹ : A) (den A x⁻¹) := (associated_den_num_inv x⁻¹ (inv_ne_zero hx)).symm
  rw [inv_inv] at this
  exact this

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