toFractionRing_inj — Mathlib

English

Equality in the fraction ring after applying toFractionRing implies equality of RatFunc elements.

Русский

Равенство после применения toFractionRing приводит к равенству соответствующих RatFunc.

LaTeX

$$$\\text{toFractionRing}(x) = \\text{toFractionRing}(y) \\iff x = y$$$

Lean4

@[simp]
theorem toFractionRing_inj {x y : RatFunc K} : toFractionRing x = toFractionRing y ↔ x = y :=
  toFractionRing_injective.eq_iff

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