English
For all x, y in R, (x : ℍ[R]) = (y : ℍ[R]) if and only if x = y; the coercion is injective.
Русский
Для всех x, y \\in R выполняется (x \\in \\mathbb{H}(R)) = (y \\in \\mathbb{H}(R)) тогда и только тогда, когда x = y; вложение инъективно.
LaTeX
$$$\\forall x \\forall y \\in R, (x : \\mathbb{H}(R)) = (y : \\mathbb{H}(R)) \\Leftrightarrow x = y$$$
Lean4
@[simp]
theorem coe_inj {x y : R} : (x : ℍ[R]) = y ↔ x = y :=
coe_injective.eq_iff