num_mul_den_eq_num_mul_den_iff_eq

English

Equivalent formulation of the previous relation with roles swapped.

Русский

Эквивалентная формулировка предыдущего со сменой ролей.

LaTeX

$$$\\mathrm{num}_A(x) \\cdot \\mathrm{den}_A(y) = \\mathrm{num}_A(y) \\cdot \\mathrm{den}_A(x) \\iff x = y$$$

Lean4

theorem num_mul_den_eq_num_mul_den_iff_eq {x y : K} : num A y * den A x = num A x * den A y ↔ x = y :=
  ⟨fun h ↦ by simpa only [mk'_num_den] using mk'_eq_of_eq' (S := K) h, fun h ↦ by rw [h]⟩

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