num_mul_den_eq_num_iff_eq' — Mathlib

English

For y ∈ K, the relation num_A(y)·den_A(x) = num_A(x)·den_A(y) characterizes y = x.

Русский

Для y ∈ K равенство num_A(y)·den_A(x) = num_A(x)·den_A(y) эквивалентно y = x.

LaTeX

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

Lean4

theorem num_mul_den_eq_num_iff_eq' {x y : K} : y * algebraMap A K (den A x) = algebraMap A K (num A x) ↔ x = y :=
  ⟨fun h ↦ by simpa only [eq_comm, mk'_num_den] using eq_mk'_iff_mul_eq.mpr h, fun h ↦
    eq_mk'_iff_mul_eq.mp (by rw [h, mk'_num_den])⟩

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