ext_rat' — Mathlib

English

If two monoid-with-zero homs from Rat to M₀ agree on the integers, then they are equal.

Русский

Если два гомоморфизма моноида с нулём из Rat в M₀ совпадают на целых, то они равны.

LaTeX

$$$\text{ext}_\text{rat} : \forall f,g : ℚ →*₀ M₀,\ (f \circ \text{Int.castRingHom}) = (g \circ \text{Int.castRingHom}) \Rightarrow f = g.$$$

Lean4

/-- If monoid with zero homs `f` and `g` from `ℚ` agree on the integers then they are equal. -/
theorem ext_rat' (h : ∀ m : ℤ, f m = g m) : f = g :=
  (DFunLike.ext f g) fun r =>
    by
    rw [← r.num_div_den, div_eq_mul_inv, map_mul, map_mul, h, ← Int.cast_natCast, eq_on_inv₀ f g]
    apply h

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