English
If two ring homs from Rat to a semiring agree on the integers, they are equal.
Русский
Если два кольцевых гомоморфизма из Rat в полукольцо согласуются на целых, то они равны.
LaTeX
$$$\text{ext\_rat} : \forall f,g : Rat → R,\ (f \circ Int.cast) = (g \circ Int.cast) \Rightarrow f = g.$$$
Lean4
/-- Any two ring homomorphisms from `ℚ` to a semiring are equal. If the codomain is a division ring,
then this lemma follows from `eq_ratCast`. -/
theorem ext_rat {R : Type*} [Semiring R] [FunLike F ℚ R] [RingHomClass F ℚ R] (f g : F) : f = g :=
MonoidWithZeroHomClass.ext_rat' <|
RingHom.congr_fun <| ((f : ℚ →+* R).comp (Int.castRingHom ℚ)).ext_int ((g : ℚ →+* R).comp (Int.castRingHom ℚ))
