English
The association between denominator and inverse numerator persists under the inverse map as in 180488.
Русский
Ассоциированность деноминатора и числителя обратного элемента сохраняется в обратном отображении.
LaTeX
$$$\\mathrm{Associated}(\\mathrm{den}_A(x), \\mathrm{num}_A(x^{-1}))$$$
Lean4
theorem associated_den_num_inv (x : K) (hx : x ≠ 0) : Associated (den A x : A) (num A x⁻¹) :=
associated_of_dvd_dvd
(IsRelPrime.dvd_of_dvd_mul_right (IsFractionRing.num_den_reduced A x).symm <|
dvd_of_mul_left_dvd (a := (den A x⁻¹ : A)) <|
dvd_of_eq <|
FaithfulSMul.algebraMap_injective A K <| Eq.symm <| eq_of_div_eq_one (by simp [mul_div_mul_comm, hx]))
(IsRelPrime.dvd_of_dvd_mul_right (IsFractionRing.num_den_reduced A x⁻¹) <|
dvd_of_mul_left_dvd (a := (num A x : A)) <|
dvd_of_eq <| FaithfulSMul.algebraMap_injective A K <| eq_of_div_eq_one (by simp [mul_div_mul_comm, hx]))
